/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRK30/FONT#10=ZERO30
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ H


␈↓ ↓H␈↓α␈↓ α$REPRESENTATION OF RECURSIVE PROGRAMS IN FIRST ORDER LOGIC

␈↓ ↓H␈↓α␈↓ ¬Jby John McCarthy











␈↓ ↓H␈↓␈↓ α_This␈αpaper␈αpresents␈αmethods␈αof␈αrepresenting␈αrecursive␈αprograms␈αby␈αsentences␈αand␈αschemata
␈↓ ↓H␈↓of␈α
first␈α
order␈α
logic,␈α
characterization␈α
of␈α
␈↓↓recursion␈α
induction␈↓,␈α
␈↓↓subgoal␈α
induction␈↓,␈α∞␈↓↓inductive␈α
assertions␈↓
␈↓ ↓H␈↓and␈α⊂other␈α⊂ways␈α⊂of␈α⊂proving␈α⊂facts␈α⊂about␈α⊂programs␈α⊂as␈α⊂axiom␈α⊂schemata␈α⊂of␈α⊂first␈α⊂order␈α⊂logic,␈α∂and
␈↓ ↓H␈↓applications of these results to proving assertions about programs.
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 91


␈↓ ↓H␈↓α1. Introduction and Motivation.

␈↓ ↓H␈↓␈↓ α_It␈α
has␈αbeen␈α
concluded␈αfrom␈α
the␈α
undecideability␈αof␈α
both␈αequivalence␈α
and␈αnon-equivalence␈α
of
␈↓ ↓H␈↓abstract␈α⊃recursive␈α⊃program␈α⊃schemata␈α⊃that␈α⊃recursive␈α⊃programs␈α⊃cannot␈α⊃be␈α⊃characterized␈α⊃in␈α⊂first
␈↓ ↓H␈↓order␈α⊂logic.␈α⊃ Cooper␈α⊂(1969)␈α⊂showed␈α⊃how␈α⊂to␈α⊂characterize␈α⊃them␈α⊂in␈α⊂second␈α⊃order␈α⊂logic,␈α⊃and␈α⊂that
␈↓ ↓H␈↓seemed␈α∪to␈α∩settle␈α∪the␈α∪matter.␈α∩ However,␈α∪we␈α∩will␈α∪exhibit␈α∪first␈α∩order␈α∪characterizations␈α∪that␈α∩are
␈↓ ↓H␈↓incomplete␈α∞only␈α∞in␈α∞that␈α∞they␈α∞admit␈α∞non-standard␈α∞models␈α∞like␈α∞those␈α∞of␈α∞first␈α∞order␈α∞arithmetic.␈α
 It
␈↓ ↓H␈↓now␈αseems␈αlikely␈αthat␈αall␈α"ordinary"␈αassertions␈αabout␈αprograms␈αwill␈αbe␈αprovable␈αor␈αdisprovable␈αin
␈↓ ↓H␈↓first order theories.

␈↓ ↓H␈↓␈↓ α_Beyond␈α∂illuminating␈α∂the␈α⊂logical␈α∂structure␈α∂of␈α∂computer␈α⊂programs,␈α∂these␈α∂results␈α⊂have␈α∂some
␈↓ ↓H␈↓practical␈α⊂significance.␈α⊂ First,␈α⊂the␈α⊂correctness␈α⊂of␈α∂a␈α⊂computer␈α⊂program␈α⊂often␈α⊂involves␈α⊂facts␈α∂about
␈↓ ↓H␈↓other␈α
mathematical␈α
domains,␈α
and␈α
these␈α
are␈α
often␈α
conveniently␈α
expressed␈α
in␈α
first␈α
order␈α
logic␈α
or␈αin␈α
a
␈↓ ↓H␈↓set␈α∂theory␈α∂axiomatized␈α∂in␈α∂first␈α∂order␈α∂logic.␈α∂ It␈α∂has␈α∂proved␈α∂particularly␈α∂difficult␈α∂to␈α⊂work␈α∂within
␈↓ ↓H␈↓logics␈αthat␈αadmit␈α
only␈αcontinuous␈αfunctions␈αand␈α
predicates.␈α Second,␈αproof-checking␈α
and␈αtheorem
␈↓ ↓H␈↓proving␈αprograms␈αhave␈αbeen␈αdeveloped␈αfor␈αfirst␈αorder␈αlogic.␈α Finally,␈αfirst␈αorder␈αlogic␈αis␈αcomplete,
␈↓ ↓H␈↓so␈α∞that␈α∞the␈α∂G␈↓
:␈↓odelian␈α∞incompleteness␈α∞of␈α∂any␈α∞theory␈α∞is␈α∞in␈α∂the␈α∞set␈α∞of␈α∂axioms␈α∞and␈α∞can␈α∂be␈α∞reduced
␈↓ ↓H␈↓when necessary by adding axioms rather than by changing the logical system.

␈↓ ↓H␈↓␈↓ α_While␈α↔our␈α↔goal␈α↔is␈α⊗first␈α↔order␈α↔representations␈α↔of␈α⊗recursive␈α↔programs,␈α↔we␈α↔will␈α⊗make
␈↓ ↓H␈↓considerable informal use of higher order functionals and predicates.

␈↓ ↓H␈↓␈↓ α_We␈α⊗present␈α↔two␈α⊗methods␈α↔of␈α⊗representing␈α↔recursive␈α⊗programs.␈α↔ The␈α⊗first␈α↔involves␈α⊗a
␈↓ ↓H␈↓␈↓↓functional␈α∞equation␈↓␈α∞and␈α∞a␈α∞␈↓↓minimization␈α∞schema␈↓␈α∞for␈α∞each␈α∞program.␈α∞ The␈α∞functional␈α∞equation␈α∞has
␈↓ ↓H␈↓the␈αfunction␈αon␈αboth␈αsides␈αof␈αan␈αequality␈αsign␈αand␈αso␈αdefines␈αit␈αimplicitly.␈α However,␈αall␈αvariables
␈↓ ↓H␈↓are␈α∞universally␈α∞quantified.␈α∞ The␈α∞second␈α∂approach␈α∞defines␈α∞the␈α∞function␈α∞explicitly,␈α∂but␈α∞existential
␈↓ ↓H␈↓quantifiers␈α
asserting␈α
the␈αexistence␈α
of␈α
finite␈αapproximations␈α
to␈α
the␈αfunction␈α
occur␈α
in␈α
the␈αformula.
␈↓ ↓H␈↓The␈α
fact␈α
that␈α
the␈α
functional␈α
equation␈α
of␈α
a␈α
program␈α
not␈α
known␈α
to␈α
terminate␈α
can␈α
nevertheless␈αbe
␈↓ ↓H␈↓written␈αso␈αsimply␈αin␈αfirst␈αorder␈αlogic␈αwas␈αfirst␈αdiscovered␈αby␈αCartwright␈α(1977),␈αbut␈αthe␈αremaining
␈↓ ↓H␈↓results seem to be new.


␈↓ ↓H␈↓α2. Recursive Programs.

␈↓ ↓H␈↓␈↓ α_An␈α
adequate␈α
background␈α
for␈α
this␈α
paper␈α
is␈α
contained␈α
in␈α
(Manna␈α
1974)␈α
and␈α
more␈α
concisely␈α
in
␈↓ ↓H␈↓(Manna,␈α∂Ness␈α∞and␈α∂Vuillemin␈α∞1973).␈α∂ The␈α∞connections␈α∂of␈α∞recursive␈α∂programs␈α∞with␈α∂second␈α∞order
␈↓ ↓H␈↓logic are given in (Cooper 1969) and (Park 1970).

␈↓ ↓H␈↓␈↓ α_We shall consider mainly ␈↓↓recursive programs␈↓ of the general form

␈↓ ↓H␈↓1)␈↓ α8  ␈↓↓f(x) ← ␈↓	t␈↓↓[f](x)␈↓,

␈↓ ↓H␈↓where ␈↓	t␈↓ is a ␈↓↓computable functional␈↓ like

␈↓ ↓H␈↓2)␈↓ α8  ␈↓↓␈↓	t␈↓↓ = λf.λx.(␈↓αif␈↓↓ x = 0 ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ x . f(x - 1))␈↓,

␈↓ ↓H␈↓which gives rise to the well known recursive definition of the factorial function, namely

␈↓ ↓H␈↓3)␈↓ α8  ␈↓↓n! ← ␈↓αif␈↓↓ n = 0 ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ n . (n - 1)!␈↓.
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 92


␈↓ ↓H␈↓␈↓ α_In␈α
general,␈α
we␈α
shall␈α
be␈αinterested␈α
in␈α
partial␈α
functions␈α
from␈αa␈α
domain␈α
D1␈α
to␈α
a␈α
domain␈αD2,
␈↓ ↓H␈↓and␈α
it␈α
will␈α
often␈αbe␈α
necessary␈α
to␈α
augment␈αthese␈α
domains␈α
by␈α
an␈αundefined␈α
element␈α
denoted␈α
by␈α␈↓	w␈↓
␈↓ ↓H␈↓giving␈αrise␈αto␈αdomains␈αD1␈↓∧+␈↓␈αand␈αD2␈↓∧+␈↓.␈α A␈αset␈α␈↓↓F␈↓␈αof␈αtotal␈αbase␈αfunctions␈αon␈αthe␈αdomains␈α
is␈αassumed
␈↓ ↓H␈↓available, and we study functions ␈↓↓computable in the set F␈↓.

␈↓ ↓H␈↓␈↓ α_It␈αis␈αimportant␈αto␈αdistinguish␈αbetween␈αa␈αprogram␈αas␈αa␈αtext␈αand␈αthe␈αpartial␈αfunction␈αdefined
␈↓ ↓H␈↓by␈α⊃the␈α⊃program␈α⊂when␈α⊃one␈α⊃is␈α⊂interested␈α⊃in␈α⊃describing␈α⊂the␈α⊃dependence␈α⊃of␈α⊂the␈α⊃function␈α⊃on␈α⊂the
␈↓ ↓H␈↓interpretation␈α
of␈α
the␈α
basic␈αfunction␈α
and␈α
predicate␈α
symbols.␈α
 However,␈αwe␈α
will␈α
be␈α
working␈αwith␈α
just
␈↓ ↓H␈↓one␈α
interpretation␈α
at␈αa␈α
time,␈α
so␈αwe␈α
won't␈α
use␈αseparate␈α
symbols␈α
for␈αprograms␈α
and␈α
the␈αfunctions␈α
they
␈↓ ↓H␈↓determine.


␈↓ ↓H␈↓α3. The Functional Equation of a Recursive Program.

␈↓ ↓H␈↓␈↓ α_Consider the Lisp program

␈↓ ↓H␈↓4)␈↓ α8  ␈↓↓subst[x,y,z] ← ␈↓αif␈↓↓ ␈↓αat␈↓↓ z ␈↓αthen␈↓↓ [␈↓αif␈↓↓ z=y ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ z] ␈↓αelse␈↓↓ subst[x,y,␈↓αa␈↓↓ z] . subst[x,y,␈↓αd␈↓↓ z]␈↓.

␈↓ ↓H␈↓The␈α
above␈α
is␈α
in␈α
Lisp␈α
␈↓↓external␈↓␈α
or␈α
␈↓↓publication␈↓␈α
notation␈α
in␈α
which␈α
 ␈↓αa␈↓ ␈↓↓x␈↓ ␈α
(bold␈α
face␈α
␈↓αa␈↓)␈α
stands␈α
for␈α
␈↓↓car[x]␈↓,
␈↓ ↓H␈↓ ␈↓αd␈↓ ␈↓↓x␈↓ ␈α∂for␈α∂␈↓↓cdr[x]␈↓,␈α⊂ ␈↓↓x . y␈↓ ␈α∂for␈α∂␈↓↓cons[x,y]␈↓,␈α∂ ␈↓αat␈↓ ␈↓↓x␈↓ ␈α⊂for␈α∂␈↓↓atom[x]␈↓,␈α∂ ␈↓αn␈↓ ␈↓↓x␈↓ ␈α∂for␈α⊂␈↓↓null[x]␈↓,␈α∂and␈α∂␈↓↓<x␈↓β1␈↓↓␈α∂...␈α⊂x␈↓βn␈↓>␈α∂for
␈↓ ↓H␈↓␈↓↓list[x␈↓β1␈↓↓,␈α
...␈α
,x␈↓βn␈↓],␈α
and␈α
␈↓↓x * y␈↓␈α
for␈α
␈↓↓append[x,y]␈↓.␈α
 Equality␈α
is␈α
taken␈α
as␈α
equality␈α
of␈α
S-expressions␈αso␈α
that
␈↓ ↓H␈↓␈↓αeq␈↓ is not used.  The program is written

␈↓ ↓H␈↓␈↓ α_(DE␈αSUBST␈α(X␈αY␈αZ)␈α(COND␈α((ATOM␈αZ)␈α(COND␈α((EQUAL␈αZ␈αY)␈αX)␈α(T␈αZ)))␈α(T␈α(CONS
␈↓ ↓H␈↓(SUBST X Y (CAR Z)) (SUBST X Y (CDR Z))))))

␈↓ ↓H␈↓in Lisp ␈↓↓internal notation␈↓.

␈↓ ↓H␈↓␈↓ α_The␈α∞basic␈α
functions␈α∞{␈↓↓car,␈α
cdr,␈α∞cons,␈α
atom}␈↓␈α∞of␈α∞Lisp␈α
are␈α∞all␈α
assumed␈α∞total,␈α
but␈α∞we␈α∞will␈α
say
␈↓ ↓H␈↓nothing␈α∞about␈α∞the␈α∞values␈α∞of␈α∞␈↓↓car␈↓␈α∞and␈α∞␈↓↓cdr␈↓␈α∞when␈α∞applied␈α∞to␈α∞atoms.␈α∞ According␈α∞to␈α∞the␈α∞fixed␈α∞point
␈↓ ↓H␈↓theory␈α
of␈α
recursive␈α
programs,␈α
this␈α
program␈α
defines␈α
a␈α
function␈α
from␈α
␈↓↓Sexp␈↓␈α
(the␈α
set␈αof␈α
S-expressions)
␈↓ ↓H␈↓to␈αSexp␈↓∧+␈↓␈α(the␈αset␈αof␈αS-expressions␈αaugmented␈αby␈α␈↓	w␈↓).␈α This␈αfunction␈αcan␈αbe␈αcomputed␈αby␈αany␈α␈↓↓safe
␈↓ ↓H␈↓↓computation␈α⊃rule␈↓,␈α⊃(in␈α∩the␈α⊃terminology␈α⊃of␈α∩Manna,␈α⊃Ness,␈α⊃and␈α∩Vuillemin␈α⊃(1973)),␈α⊃and␈α∩when␈α⊃the
␈↓ ↓H␈↓computation␈α
terminates,␈αits␈α
value␈αwill␈α
belong␈αto␈α
␈↓↓Sexp.␈↓␈α When␈α
the␈αcomputation␈α
doesn't␈αterminate,
␈↓ ↓H␈↓the␈αvalue␈αof␈α␈↓↓f(x)␈↓␈αis␈α␈↓	w␈↓.␈α While␈αthe␈αparticular␈αfunction␈α␈↓↓subst␈↓␈αalways␈αterminates,␈αwe␈αdo␈αnot␈αassume␈αit
␈↓ ↓H␈↓in␈α∩writing␈α⊃our␈α∩first␈α⊃order␈α∩formula.␈α⊃ Indeed␈α∩we␈α⊃can␈α∩use␈α⊃the␈α∩first␈α⊃order␈α∩formula␈α⊃to␈α∩prove␈α⊃by
␈↓ ↓H␈↓structural induction that ␈↓↓subst␈↓ is total.

␈↓ ↓H␈↓␈↓ α_These facts show that the function ␈↓↓subst␈↓ defined recursively by (4) satisfies the sentence

␈↓ ↓H␈↓5)␈↓ α8␈α⊃ ␈↓↓∀x␈α⊃y␈α⊃z.(subst(x,y,z)␈α⊃=␈α⊂␈↓αif␈↓↓␈α⊃␈↓αat␈↓↓␈α⊃z␈α⊃␈↓αthen␈↓↓␈α⊃(␈↓αif␈↓↓␈α⊂z␈α⊃=␈α⊃y␈α⊃␈↓αthen␈↓↓␈α⊃x␈α⊂␈↓αelse␈↓↓␈α⊃z)␈α⊃␈↓αelse␈↓↓␈α⊃subst(x,y,␈↓αa␈↓↓␈α⊃z)␈α⊂.
␈↓ ↓H␈↓↓subst(x,y,␈↓αd␈↓↓ z))␈↓

␈↓ ↓H␈↓of␈α
first␈αorder␈α
logic.␈α
 The␈αvariables␈α
␈↓↓x,␈αy␈↓␈α
and␈α
␈↓↓z␈↓␈αrange␈α
over␈α␈↓↓Sexp;␈↓␈α
when␈α
we␈αwant␈α
to␈α
quantify␈αover
␈↓ ↓H␈↓␈↓↓Sexp␈↓∧+␈↓,␈α⊃we␈α⊂use␈α⊃␈↓↓X,␈α⊂Y␈α⊃␈↓and␈↓↓␈α⊂Z␈↓.␈α⊃ Moreover,␈α⊂we␈α⊃are␈α⊂augmenting␈α⊃first␈α⊂order␈α⊃logic␈α⊂(as␈α⊃described␈α⊂in
␈↓ ↓H␈↓(Manna␈α∩1975))␈α∩by␈α∩allowing␈α∩conditional␈α∩expressions␈α∩as␈α∩terms.␈α∩ The␈α∩augmentation␈α∩is␈α∩does␈α⊃not
␈↓ ↓H␈↓change␈αwhat␈αcan␈α
be␈αexpressed␈αin␈α
first␈αorder␈αlogic,␈αbecause␈α
conditional␈αexpressions␈αcan␈α
always␈αbe
␈↓ ↓H␈↓eliminated from sentences by distributing predicates over them.  Thus (5) can be written
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 93


␈↓ ↓H␈↓6)␈↓ α8␈α ␈↓↓∀x␈αy␈αz.(␈↓αat␈↓↓␈αz␈α⊃␈α(z=y␈α⊃␈αsubst(x,y,z)␈α=␈α
x)␈α∧␈αz≠y␈α⊃␈αsubst(x,y,z)␈α=␈αz)␈α∧␈α¬␈↓αat␈↓↓␈αz␈α⊃␈α
subst(x,y,z)
␈↓ ↓H␈↓↓= subst(x,y,␈↓αa␈↓↓ z) . subst(x,y,␈↓αd␈↓↓ z)),␈↓

␈↓ ↓H␈↓but␈α∞we␈α
will␈α∞use␈α
conditional␈α∞expressions,␈α
because␈α∞they␈α
are␈α∞clearer␈α
and␈α∞express␈α
the␈α∞content␈α∞of␈α
the
␈↓ ↓H␈↓recursive␈α
program␈α
directly.␈α
 In␈αfact,␈α
we␈α
recommend␈α
their␈α
admission␈αas␈α
terms␈α
in␈α
logic␈αgenerally,␈α
and
␈↓ ↓H␈↓first␈αorder␈αlogic␈αin␈αparticular.␈α They␈αdon't␈αextend␈αthe␈αlogical␈αpower,␈αbut␈αthey␈αpermit␈αmany␈αfacts␈α
to
␈↓ ↓H␈↓be expressed without circumlocution.

␈↓ ↓H␈↓␈↓ α_One␈αgoal␈αof␈α
our␈αfirst␈αorder␈α
representation␈αis␈αto␈αuse␈α
(4)␈αonly␈αto␈α
justify␈αwriting␈α(5)␈α
and␈αthen
␈↓ ↓H␈↓prove all properties of ␈↓↓subst␈↓ using a first order axiomatization of Lisp.




␈↓ ↓H␈↓α4. First Order Axioms for Lisp.

␈↓ ↓H␈↓␈↓ α_We␈α⊂use␈α⊃lower␈α⊂case␈α⊂variables␈α⊃␈↓↓x,␈↓␈α⊂␈↓↓y,␈↓␈α⊃and␈α⊂␈↓↓z␈↓␈α⊂with␈α⊃or␈α⊂without␈α⊂subscripts␈α⊃to␈α⊂range␈α⊃over␈α⊂S-
␈↓ ↓H␈↓expressions.␈α Capitalized␈αvariables␈αrange␈αover␈αall␈αentities.␈α
 We␈αalso␈αuse␈αvariables␈α␈↓↓u,␈↓␈α␈↓↓v␈↓␈αand␈α␈↓↓w␈↓␈α
with
␈↓ ↓H␈↓or␈α∂without␈α∂subscripts␈α∂to␈α∂range␈α∂over␈α∂lists,␈α∂i.e.␈α∂S-expressions␈α∂such␈α∂that␈α∂successive␈α∂␈↓↓cdr␈↓s␈α∂eventually
␈↓ ↓H␈↓reach␈αNIL.␈α (The␈α␈↓↓car␈↓␈αof␈αa␈αlist␈αis␈αnot␈αrequired␈αto␈αbe␈αa␈αlist).␈α We␈αuse␈αpredicates␈α␈↓↓issexp␈↓␈αand␈α␈↓↓islist␈↓␈αto
␈↓ ↓H␈↓assert␈α∪that␈α∪an␈α∀individual␈α∪is␈α∪an␈α∀S-expression␈α∪or␈α∪a␈α∪list.␈α∀ First␈α∪come␈α∪the␈α∀"housekeeping"␈α∪and
␈↓ ↓H␈↓"algebraic" axioms:

␈↓ ↓H␈↓L1:     ␈↓↓∀x.issexp x␈↓

␈↓ ↓H␈↓L2:     ␈↓↓∀u.islist u␈↓

␈↓ ↓H␈↓L3:     ␈↓↓∀u.issexp u␈↓

␈↓ ↓H␈↓L4:     ␈↓↓¬issexp ␈↓	w␈↓

␈↓ ↓H␈↓L5:     ␈↓↓islist ␈↓NIL

␈↓ ↓H␈↓L6:     ␈↓↓␈↓αat␈↓↓ ␈↓NIL␈↓↓␈↓

␈↓ ↓H␈↓L7:     ␈↓↓∀u.(␈↓αat␈↓↓ u ⊃ u = ␈↓NIL␈↓↓)␈↓

␈↓ ↓H␈↓L8:     ␈↓↓∀x y.issexp (x.y)␈↓

␈↓ ↓H␈↓L9:     ␈↓↓∀x u.islist (x.u)␈↓

␈↓ ↓H␈↓L10:    ␈↓↓∀x. ¬␈↓αat␈↓↓ x ⊃ issexp ␈↓αa␈↓↓ x␈↓

␈↓ ↓H␈↓L11:    ␈↓↓∀x. ¬␈↓αat␈↓↓ x ⊃ issexp ␈↓αd␈↓↓ x␈↓

␈↓ ↓H␈↓L12:    ␈↓↓∀u. u ≠ ␈↓NIL␈↓↓ ⊃ islist ␈↓αd␈↓↓ u␈↓

␈↓ ↓H␈↓L13:    ␈↓↓∀x y. ␈↓αa␈↓↓ (x.y) = x␈↓

␈↓ ↓H␈↓L14:    ␈↓↓∀x y. ␈↓αd␈↓↓ (x.y) = y␈↓
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 94


␈↓ ↓H␈↓L15:    ␈↓↓∀x y. ¬␈↓αat␈↓↓ (x.y)␈↓

␈↓ ↓H␈↓L16:    ␈↓↓∀x.¬␈↓αat␈↓↓ x ⊃ (␈↓αa␈↓↓ x . ␈↓αd␈↓↓ x) = x␈↓

␈↓ ↓H␈↓␈↓ α_Next we have axiom schemata of induction

␈↓ ↓H␈↓LS1:    ␈↓↓(∀x.␈↓αat␈↓↓ x ⊃ ␈↓	F␈↓↓ x) ∧ ∀x.(¬␈↓αat␈↓↓ x ∧ ␈↓	F␈↓↓ ␈↓αa␈↓↓ x ∧ ␈↓	F␈↓↓ ␈↓αd␈↓↓ x ⊃ ␈↓	F␈↓↓ x) ⊃ ∀x.␈↓	F␈↓↓ x␈↓

␈↓ ↓H␈↓LS2:    ␈↓↓(∀u.u = ␈↓NIL␈↓↓ ⊃ ␈↓	F␈↓↓ u) ∧ ∀u.(u ≠ ␈↓NIL␈↓↓ ∧ ␈↓	F␈↓↓ ␈↓αd␈↓↓ u ⊃ ␈↓	F␈↓↓ u) ⊃ ∀u. ␈↓	F␈↓↓ u␈↓.

␈↓ ↓H␈↓␈↓ α_From these axioms and schemata, we can prove

␈↓ ↓H␈↓7)␈↓ α8  ␈↓↓∀x y z.issexp subst(x,y,z)␈↓

␈↓ ↓H␈↓which␈α
is␈α
our␈α
way␈α
of␈α
saying␈αthat␈α
␈↓↓subst␈↓␈α
is␈α
total.␈α
 The␈α
key␈αstep␈α
is␈α
applying␈α
the␈α
axiom␈α
schema␈αLS1
␈↓ ↓H␈↓with␈α∂the␈α∂predicate␈α∞␈↓↓␈↓	F␈↓↓(z)␈α∂≡␈α∂issexp(x,y,z)␈↓.␈α∂ We␈α∞can␈α∂also␈α∂prove␈α∂in␈α∞first␈α∂order␈α∂logic␈α∂such␈α∞algebraic
␈↓ ↓H␈↓properties of ␈↓↓subst␈↓ as

␈↓ ↓H␈↓8)␈↓ α8  ␈↓↓∀x y z y1 z1.(¬occur(y,z1) ⊃ subst(subst(x,y,z),y1,z1) = subst(x,y,subst(z,y1,z1)))␈↓

␈↓ ↓H␈↓if␈αwe␈αhave␈αsuitable␈αaxiomatization␈αof␈αthe␈αpredicate␈α␈↓↓occur(x,y)␈↓␈αmeaning␈αthat␈αthe␈αatom␈α␈↓↓x␈↓␈αoccurs␈αin
␈↓ ↓H␈↓the S-expression ␈↓↓y.␈↓

␈↓ ↓H␈↓␈↓ α_The␈α
axiomatization␈α
of␈α
the␈α
predicate␈α
␈↓↓occur␈↓␈α
raises␈α
some␈α
new␈α
problems.␈α
 It␈α
is␈α
defined␈α∞by␈α
the
␈↓ ↓H␈↓recursive Lisp program

␈↓ ↓H␈↓9)␈↓ α8  ␈↓↓occur(x,y) ← (x = y) ∨ (¬␈↓αat␈↓↓ y ∧ (occur(x,␈↓αa␈↓↓ y) ∨ occur(x,␈↓αd␈↓↓ y)))␈↓.

␈↓ ↓H␈↓If␈α∂we␈α∂were␈α∂sure␈α∂in␈α∞advance␈α∂that␈α∂␈↓↓occur␈↓␈α∂were␈α∂total,␈α∂we␈α∞could␈α∂translate␈α∂the␈α∂recursion␈α∂(9)␈α∂into␈α∞the
␈↓ ↓H␈↓sentence

␈↓ ↓H␈↓10)␈↓ α8  ␈↓↓∀x y.(occur(x,y) ≡ (x = y) ∨ (¬␈↓αat␈↓↓ y ∧ (occur(x,␈↓αa␈↓↓ y) ∨ occur(x,␈↓αd␈↓↓ y))))␈↓

␈↓ ↓H␈↓which␈α⊂will␈α∂suffice␈α⊂for␈α∂proving␈α⊂(8),␈α∂but␈α⊂we␈α∂have␈α⊂no␈α∂right␈α⊂to␈α∂write␈α⊂it␈α∂down␈α⊂from␈α⊂the␈α∂recursive
␈↓ ↓H␈↓definition (9).

␈↓ ↓H␈↓␈↓ α_What we may write without proving that ␈↓↓occur␈↓ is total is an implicit definition

␈↓ ↓H␈↓11)␈↓ α8  ␈↓↓∀x y.(occura(x,y) = (x equals y) or (not atom y and (occura(x,␈↓αa␈↓↓ y) or occura(x,␈↓αd␈↓↓ y))))␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓12)␈↓ α8  ␈↓↓∀x y.(occur(x,y) ≡ (occura(x,y) = T))␈↓.

␈↓ ↓H␈↓From␈α∞(11),␈α∞we␈α∞can␈α∞prove␈α∞that␈α∞␈↓↓occura␈↓␈α∂is␈α∞total␈α∞by␈α∞structural␈α∞induction␈α∞and␈α∞from␈α∞this␈α∂(10)␈α∞quickly
␈↓ ↓H␈↓follows.

␈↓ ↓H␈↓␈↓ α_Since␈αrecursive␈αdefinitions␈αgive␈αrise␈αto␈αpartial␈α
predicates,␈αand␈αwe␈αdon't␈αwant␈αto␈αuse␈αa␈α
partial
␈↓ ↓H␈↓predicate␈α∞logic,␈α∞we␈α∞introduce␈α∂a␈α∞domain␈α∞␈↓	P␈↓␈α∞of␈α∂␈↓↓extended␈α∞truth␈α∞values␈↓␈α∞with␈α∂characteristic␈α∞predicate
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 95


␈↓ ↓H␈↓␈↓↓isetv␈↓␈α
whose␈α
elements␈α
are␈α
␈↓↓T,␈↓␈α∞␈↓↓F␈↓␈α
and␈α
␈↓	w␈↓.␈α
 There␈α
is␈α
no␈α∞harm␈α
in␈α
identifying␈α
␈↓↓T␈↓␈α
and␈α
␈↓↓F␈↓␈α∞with␈α
suitable
␈↓ ↓H␈↓Lisp␈αatoms␈αor␈αwith␈αthe␈αintegers␈α1␈αand␈α0.␈α The␈αfollowing␈αaxioms␈αdescribe␈αfunctions␈αinto␈αor␈αout␈αof
␈↓ ↓H␈↓␈↓	P␈↓↓.  We use the predicate istv␈↓ to test for the honest truth values ␈↓↓T␈↓ and ␈↓↓F.␈↓

␈↓ ↓H␈↓B1:     ␈↓↓∀p.(isetv p)␈↓

␈↓ ↓H␈↓B2:     ␈↓↓∀p.(p = T ∨ p = F ∨ p = ␈↓	w␈↓↓)␈↓

␈↓ ↓H␈↓B3:     ␈↓↓T ≠ F ∧ T ≠ ␈↓	w␈↓↓ ∧ F ≠ ␈↓	w␈↓

␈↓ ↓H␈↓B4:     ␈↓↓∀p.(istv p ≡ p = T ∨ p = F)␈↓

␈↓ ↓H␈↓B5:     ␈↓↓∀p. isetv not p␈↓

␈↓ ↓H␈↓B6:     ␈↓↓∀p q. isetv(p and q)␈↓

␈↓ ↓H␈↓B7:     ␈↓↓∀p q. isetv(p or q)␈↓

␈↓ ↓H␈↓B8:     ␈↓↓∀p.(not p = ␈↓αif␈↓↓ (p = ␈↓	w␈↓↓) ␈↓αthen␈↓↓ ␈↓	w␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ p = T ␈↓αthen␈↓↓ F ␈↓αelse␈↓↓ T)␈↓

␈↓ ↓H␈↓B9:     ␈↓↓∀p q.(p and q = ␈↓αif␈↓↓ (p = ␈↓	w␈↓↓) ␈↓αthen␈↓↓ ␈↓	w␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ p = T ␈↓αthen␈↓↓ q ␈↓αelse␈↓↓ F)␈↓

␈↓ ↓H␈↓B10:    ␈↓↓∀p q.(p or q = (␈↓αif␈↓↓ p = ␈↓	w␈↓↓) ␈↓αthen␈↓↓ ␈↓	w␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ p = T ␈↓αthen␈↓↓ T ␈↓αelse␈↓↓ q)␈↓

␈↓ ↓H␈↓B11:    ␈↓↓∀X Y.(X equal Y = ␈↓αif␈↓↓ ¬issexp X ∨ ¬issexp Y ␈↓αthen␈↓↓ ␈↓	w␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ X = Y ␈↓αthen␈↓↓ T ␈↓αelse␈↓↓ F)␈↓

␈↓ ↓H␈↓B12:    ␈↓↓∀X.(aatom X = ␈↓αif␈↓↓ ¬issexp X ␈↓αthen␈↓↓ ␈↓	w␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αat␈↓↓ X ␈↓αthen␈↓↓ T ␈↓αelse␈↓↓ F)␈↓,

␈↓ ↓H␈↓and we also need a conditional expression that can take an argument from ␈↓	P␈↓, namely

␈↓ ↓H␈↓B13:    ␈↓↓∀p X Y.(if(p,X,Y) = ␈↓αif␈↓↓ p = ␈↓	w␈↓↓ ␈↓αthen␈↓↓ ␈↓	w␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ p = T ␈↓αthen␈↓↓ X ␈↓αelse␈↓↓ Y)␈↓.

␈↓ ↓H␈↓␈↓ α_␈↓↓occura␈↓␈α
is␈α
proved␈α
total␈α
by␈α
applying␈α
schema␈αLS1␈α
with␈α
␈↓↓␈↓	F␈↓↓(y)␈α
≡␈α
occura(x,y)␈α
≠␈α
␈↓	w␈↓↓␈↓.␈α
 After␈αthis␈α
␈↓↓occur␈↓
␈↓ ↓H␈↓can be shown to satisfy (10).

␈↓ ↓H␈↓␈↓ α_The␈α∂axioms␈α∂L1-L16␈α∂and␈α∂B1-B12␈α∂together␈α∂with␈α∂the␈α∂sentences␈α∂arising␈α∂from␈α∂the␈α∂schemata
␈↓ ↓H␈↓LS1␈αand␈αLS2␈αwill␈αbe␈αcalled␈αthe␈αaxiom␈αsystem␈αLisp0.␈α We␈αwill␈αadjoin␈αone␈αmore␈αaxiom␈αlater␈αto␈αget
␈↓ ↓H␈↓the system Lisp1.

␈↓ ↓H␈↓␈↓ α_The␈αabove␈α
method␈αof␈α
replacing␈αa␈α
recursion␈αby␈αa␈α
first␈αorder␈α
sentence␈αwas␈α
first␈α(I␈αthink)␈α
used
␈↓ ↓H␈↓in (Cartwright 1977).  I'm surprised that it wasn't invented sooner.



␈↓ ↓H␈↓α1. An Extended Example.

␈↓ ↓H␈↓␈↓ α_The␈αSAMEFRINGE␈αproblem␈αis␈αto␈αwrite␈αa␈αprogram␈αthat␈αefficiently␈αdetermines␈αwhether␈αtwo
␈↓ ↓H␈↓S-expressions␈α∞have␈α∞the␈α
same␈α∞fringe,␈α∞i.e.␈α
have␈α∞the␈α∞same␈α
atoms␈α∞in␈α∞the␈α
same␈α∞order.␈α∞ (Some␈α
people
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 96


␈↓ ↓H␈↓omit␈αthe␈αNILs␈αat␈αthe␈αends␈αof␈αlists,␈αbut␈α
we␈αwill␈αtake␈αall␈αatoms).␈α Thus␈α((A.B).C)␈αand␈α(A.(B.C))␈α
have
␈↓ ↓H␈↓the␈αsame␈αfringe,␈αnamely␈α(A␈αB␈αC).␈α The␈αobject␈αof␈αthe␈αoriginal␈αproblem␈αwas␈αto␈αprogram␈αit␈αusing␈αa
␈↓ ↓H␈↓minimum␈α
of␈α
storage,␈αand␈α
it␈α
was␈αconjectured␈α
that␈α
co-routines␈αwere␈α
necessary␈α
to␈αdo␈α
it␈α
neatly.␈α We
␈↓ ↓H␈↓shall not discuss that matter here - merely the correctness of one proposed solution.

␈↓ ↓H␈↓␈↓ α_The relevant recursive definitons are

␈↓ ↓H␈↓13)␈↓ α8  ␈↓↓fringe x ← ␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ <x> ␈↓αelse␈↓↓ fringe ␈↓αa␈↓↓ x * fringe ␈↓αd␈↓↓ x␈↓,

␈↓ ↓H␈↓where ␈↓↓u * v␈↓ denotes the result of appending the lists ␈↓↓u␈↓ and ␈↓↓v␈↓ and is defined recursively by

␈↓ ↓H␈↓14)␈↓ α8  ␈↓↓u * v ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v]␈↓.

␈↓ ↓H␈↓We are interested in the condition ␈↓↓fringe x = fringe y␈↓.

␈↓ ↓H␈↓␈↓ α_The function to be proved correct is ␈↓↓samefringe[x,y]␈↓ defined by the simultaneous recursion

␈↓ ↓H␈↓15)␈↓ α8  ␈↓↓samefringe[x, y] ← (x = y) ∨ [¬␈↓αat␈↓↓ x ∧ ¬␈↓αat␈↓↓ y ∧ same[gopher x, gopher y]]␈↓,

␈↓ ↓H␈↓16)␈↓ α8  ␈↓↓same[x, y] ← (␈↓αa␈↓↓ x = ␈↓αa␈↓↓ y) ∧ samefringe[␈↓αd␈↓↓ x, ␈↓αd␈↓↓ y]␈↓,

␈↓ ↓H␈↓where

␈↓ ↓H␈↓17)␈↓ α8  ␈↓↓gopher x ←  ␈↓αif␈↓↓ ␈↓αat␈↓↓ ␈↓αa␈↓↓ x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ gopher ␈↓αaa␈↓↓ x . [␈↓αda␈↓↓ x . ␈↓αd␈↓↓ x]␈↓.

␈↓ ↓H␈↓␈↓ α_We need to prove that ␈↓↓samefringe␈↓ is total and

␈↓ ↓H␈↓18)␈↓ α8  ␈↓↓∀xy.(samefringe[x,y] ≡ fringe x = fringe y)␈↓.

␈↓ ↓H␈↓␈↓ α_The␈αminimization␈α
schemata␈αof␈α
these␈αfunctions␈α
are␈αirrelevant,␈α
because␈αwe␈α
will␈αprove␈αthat␈α
the
␈↓ ↓H␈↓functions␈αare␈αall␈αtotal␈αexcept␈αthat␈αwe␈αwon't␈αprove␈αanything␈αabout␈αthe␈αresult␈αof␈αapplying␈α␈↓↓gopher␈↓␈αto
␈↓ ↓H␈↓an atom.  The functional equations are

␈↓ ↓H␈↓19)␈↓ α8  ␈↓↓∀x.(fringe x = ␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ <x> ␈↓αelse␈↓↓ fringe ␈↓αa␈↓↓ x * fringe ␈↓αd␈↓↓ x␈↓),

␈↓ ↓H␈↓20)␈↓ α8  ␈↓↓∀u v.(u * v = ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v])␈↓.

␈↓ ↓H␈↓21)␈↓ α8␈α∂ ␈↓↓∀x␈α∂y.(samefringe[x,␈α∂y]␈α∂=␈α⊂x␈α∂equal␈α∂y␈α∂or␈α∂[not␈α∂aat␈α⊂x␈α∂and␈α∂not␈α∂aat␈α∂y␈α∂and␈α⊂same[gopher␈α∂x,
␈↓ ↓H␈↓↓gopher y]])␈↓,

␈↓ ↓H␈↓22)␈↓ α8 ␈↓↓∀x y.(same[x, y] = ␈↓αa␈↓↓ x equal ␈↓αa␈↓↓ y and samefringe[␈↓αd␈↓↓ x, ␈↓αd␈↓↓ y]␈↓,

␈↓ ↓H␈↓23)␈↓ α8 ␈↓↓∀x.(gopher x =  ␈↓αif␈↓↓ ␈↓αat␈↓↓ ␈↓αa␈↓↓ x ␈↓αthen␈↓↓ u ␈↓αelse␈↓↓ gopher ␈↓αaa␈↓↓ x . [␈↓αda␈↓↓ x . ␈↓αd␈↓↓ x])␈↓.

␈↓ ↓H␈↓Note␈α∞that␈α
because␈α∞␈↓↓samefringe␈↓␈α
and␈α∞␈↓↓same␈↓␈α
are␈α∞recursively␈α
defined␈α∞predicates␈α
which␈α∞have␈α∞not␈α
been
␈↓ ↓H␈↓proved␈α
total,␈α
their␈α
functional␈α
equations␈α
must␈α
use␈α
the␈α
imitation␈α
propositional␈α∞functions␈α
involving
␈↓ ↓H␈↓the extended truth values.

␈↓ ↓H␈↓␈↓ α_We␈αshall␈αnot␈α
give␈αfull␈αproofs␈αbut␈α
merely␈αthe␈αinduction␈αpredicates␈α
and␈αa␈αfew␈α
indications␈αof
␈↓ ↓H␈↓the algebraic transformations.  We begin with a lemma about ␈↓↓gopher␈↓.
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 97


␈↓ ↓H␈↓24)␈↓ α8 ␈↓↓∀x y.(issexp gopher[x.y] ∧ ␈↓αat␈↓↓ ␈↓αa␈↓↓ gopher[x.y] ∧ fringe gopher[x.y] = fringe[x.y])␈↓.

␈↓ ↓H␈↓␈↓ α_This lemma can be proved by S-expression structural induction using the predicate

␈↓ ↓H␈↓25)␈↓ α8 ␈↓↓P(x) ≡ ∀y.ok(x,y)␈↓,

␈↓ ↓H␈↓where ␈↓↓ok(x,y)␈↓ is defined by

␈↓ ↓H␈↓26)␈↓ α8␈↓↓∀x y.(ok(x,y) ≡ issexp gopher[x.y] ∧ ␈↓αat␈↓↓ ␈↓αa␈↓↓ gopher[x.y] ∧ fringe gopher[x.y] = fringe[x.y])␈↓.

␈↓ ↓H␈↓In␈α#the␈α#course␈α"of␈α#the␈α#proof,␈α#we␈α"use␈α#the␈α#associativity␈α"of␈α#*␈α#and␈α#the␈α"formula
␈↓ ↓H␈↓␈↓↓fringe[x.y] = fringe x * fringe y␈↓.␈α
 The␈α
lemma␈α
was␈α
expressed␈α
using␈α
␈↓↓gopher[x.y]␈↓␈α
in␈α
order␈α∞to␈α
avoid
␈↓ ↓H␈↓considering␈α
atomic␈αarguments␈α
for␈α␈↓↓gopher␈↓,␈α
but␈αit␈α
could␈α
have␈αequally␈α
well␈αbe␈α
proved␈αabout␈α
␈↓↓gopher x␈↓
␈↓ ↓H␈↓with the condition ␈↓↓¬␈↓αat␈↓↓ x␈↓.

␈↓ ↓H␈↓␈↓ α_Another␈αproof␈αcan␈αbe␈αgiven␈αusing␈αthe␈αcourse-of-values␈αinduction␈αschema␈αfor␈αintegers.␈α We
␈↓ ↓H␈↓write this schema

␈↓ ↓H␈↓ICV:    ␈↓↓∀n.(∀m.(m < n ⊃ P(m)) ⊃ P(n)) ⊃ ∀n.P(n)␈↓,

␈↓ ↓H␈↓where␈α␈↓↓m␈↓␈αand␈α␈↓↓n␈↓␈α
range␈αover␈αnon-negative␈αintegers.␈α
 Exactly␈αthe␈αsame␈αschema␈α
expresses␈αtransfinite
␈↓ ↓H␈↓induction;␈αwe␈α
need␈αonly␈α
imagine␈αthe␈αvariables␈α
ranging␈αover␈α
all␈αordinals␈αless␈α
than␈αa␈α
given␈αone␈α-␈α
in
␈↓ ↓H␈↓this case ␈↓	w␈↓, but equally well ␈↓	w␈↓␈↓	␈↓#
w␈↓#␈↓ or ε␈↓β0␈↓.  We also use the function ␈↓↓size x␈↓ defined by

␈↓ ↓H␈↓27)␈↓ α8 ␈↓↓size x ← ␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ size ␈↓αa␈↓↓ x + size ␈↓αd␈↓↓ x␈↓

␈↓ ↓H␈↓satisfying the obvious functional equation.  Our induction predicate is then

␈↓ ↓H␈↓28)␈↓ α8 ␈↓↓P(n) ≡ ∀x y.(size x = n ⊃ ok(x,y))␈↓.

␈↓ ↓H␈↓␈↓ α_For our proof about ␈↓↓samefringe␈↓ we need one more lemma about ␈↓↓gopher␈↓, namely

␈↓ ↓H␈↓29)␈↓ α8 ␈↓↓∀x y.(size gopher[x.y] = size[x.y]␈↓.

␈↓ ↓H␈↓␈↓ α_This␈α→can␈α_be␈α→proved␈α→by␈α_either␈α→of␈α_the␈α→above␈α→inductive␈α_methods␈α→or␈α→by␈α_including
␈↓ ↓H␈↓␈↓↓size gopher[x.y] = size[x.y]␈↓ in the induction hypothesis ␈↓↓ok[x,y]␈↓.

␈↓ ↓H␈↓␈↓ α_The statement about samefringe is

␈↓ ↓H␈↓30)␈↓ α8 ␈↓↓∀x y.(issexp samefringe[x,y] ∧ samefringe[x,y] = T ≡ fringe x = fringe y)␈↓,

␈↓ ↓H␈↓and it is most easily proved by induction on ␈↓↓size x + size y␈↓ using the predicate

␈↓ ↓H␈↓31)␈↓ α8␈α␈↓↓P(n)␈α≡␈α
∀x␈αy.(n␈α=␈α
size␈αx␈α+␈α
size␈αy␈α⊃␈α
issexp␈αsamefringe[x,y]␈α∧␈α
(samefringe[x,y]␈α=␈αT␈α≡␈α
fringe
␈↓ ↓H␈↓↓x = fringe y))␈↓.

␈↓ ↓H␈↓It␈α
can␈αalso␈α
be␈αproved␈α
using␈α
the␈αwell-foundedness␈α
of␈αlexicographic␈α
ordering␈α
of␈αthe␈α
list␈α␈↓↓<x␈α
␈↓αa␈↓↓␈αx>␈↓,␈α
but
␈↓ ↓H␈↓then we must decide what lexicographic orderings to include in our axiom system.
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 98


␈↓ ↓H␈↓␈↓ α_Transfinite␈α
induction␈α
is␈α∞also␈α
useful,␈α
and␈α∞can␈α
be␈α
illustrated␈α∞with␈α
a␈α
variant␈α∞␈↓↓samefringe␈↓␈α
that
␈↓ ↓H␈↓does everything in one complicated recursive definition, namely

␈↓ ↓H␈↓32)␈↓ α8␈α␈↓↓samefringe[x,y]␈α=␈α(x␈αequal␈α
y)␈αor␈αnot␈αaat␈αx␈αand␈α
not␈αaat␈αy␈αand␈α[␈↓αif␈↓↓␈α␈↓αat␈↓↓␈α
␈↓αa␈↓↓␈αx␈α␈↓αthen␈↓↓␈α[␈↓αif␈↓↓␈α␈↓αat␈↓↓␈αy␈α
␈↓αthen␈↓↓
␈↓ ↓H␈↓↓␈↓αa␈↓↓␈α
x␈α
equal␈α
␈↓αa␈↓↓␈α
y␈α
and␈α
samefringe[␈↓αd␈↓↓␈α
x,␈α
␈↓αd␈↓↓␈α
y]␈α
␈↓αelse␈↓↓␈α
samefringe[x,␈α
␈↓αaa␈↓↓␈α
y␈α
.␈α
[␈↓αda␈↓↓␈α
y␈α
.␈α
␈↓αd␈↓↓␈α
y]]]␈α
␈↓αelse␈↓↓␈αsamefringe[␈↓αaa␈↓↓␈α
x
␈↓ ↓H␈↓↓. [␈↓αda␈↓↓ x .␈↓αd␈↓↓ x], y]␈↓.

␈↓ ↓H␈↓The transfinite induction predicate then has the form

␈↓ ↓H␈↓33)␈↓ α8␈α∂␈↓↓P(n)␈α∞≡␈α∂∀x␈α∞y.[n␈α∂=␈α∂␈↓	w␈↓↓(size␈α∞x␈α∂+␈α∞size␈α∂y)␈α∂+␈α∞size␈α∂␈↓αa␈↓↓␈α∞x␈α∂+␈α∂size␈α∞␈↓αa␈↓↓␈α∂y␈α∞⊃␈α∂issexp␈α∂samefringe[x,y]␈α∞∧
␈↓ ↓H␈↓↓(samefringe[x,y] = T ≡ fringe x = fringe y)]␈↓,

␈↓ ↓H␈↓where in this formula ␈↓	w␈↓ denotes the least transfinite ordinal.

␈↓ ↓H␈↓␈↓ α_We␈α↔would␈α↔like␈α↔to␈α↔prove␈α↔that␈α↔the␈α↔amount␈α↔of␈α↔storage␈α↔used␈α↔in␈α↔the␈α↔computation␈α⊗of
␈↓ ↓H␈↓␈↓↓samefringe[x,y]␈↓␈α
aside␈α∞from␈α
that␈α∞occupied␈α
by␈α∞␈↓↓x␈↓␈α
and␈α
␈↓↓y␈↓␈α∞never␈α
exceeds␈α∞the␈α
sum␈α∞of␈α
the␈α∞numbers␈α
of
␈↓ ↓H␈↓␈↓↓car␈↓s␈αrequired␈αto␈α
reach␈αcorresponding␈αatoms␈α
in␈α␈↓↓x␈↓␈αand␈α
␈↓↓y.␈↓␈α Unfortunately,␈αwe␈α
can't␈αeven␈αexpress␈α
that
␈↓ ↓H␈↓fact,␈αbecause␈αwe␈α
are␈αaxiomatizing␈αthe␈αprograms␈α
as␈αfunctions,␈αand␈αthe␈α
amount␈αof␈αstorage␈αused␈α
does
␈↓ ↓H␈↓not␈α∞depend␈α∞merely␈α∞on␈α∂the␈α∞function␈α∞being␈α∞computed;␈α∞it␈α∂depends␈α∞on␈α∞the␈α∞method␈α∂of␈α∞computation.
␈↓ ↓H␈↓We␈α⊂may␈α∂regard␈α⊂such␈α∂things␈α⊂as␈α⊂␈↓↓intensional␈↓␈α∂properties,␈α⊂but␈α∂the␈α⊂correspondence␈α⊂with␈α∂intensional
␈↓ ↓H␈↓properties in intensional logic remains to be established.


␈↓ ↓H␈↓α2. The Minimization Schema.

␈↓ ↓H␈↓␈↓ α_The␈αfunctional␈αequation␈α
of␈αa␈αprogram␈αdoesn't␈α
completely␈αcharacterize␈αit.␈α For␈α
example,␈αthe
␈↓ ↓H␈↓program

␈↓ ↓H␈↓34)␈↓ α8 ␈↓↓f1 x ← f1 x␈↓

␈↓ ↓H␈↓leads to the sentence

␈↓ ↓H␈↓35)␈↓ α8 ␈↓↓∀x.(f1 x = f1 x)␈↓

␈↓ ↓H␈↓which␈αprovides␈α
no␈αinformation␈α
although␈αthe␈α
function␈α␈↓↓f␈↓␈α
is␈αundefined␈α
for␈αall␈α
␈↓↓x.␈↓␈α This␈α
is␈αnot␈α
always
␈↓ ↓H␈↓the case, since the program

␈↓ ↓H␈↓36)␈↓ α8 ␈↓↓f2 x ← (f2 x).␈↓NIL␈↓↓␈↓

␈↓ ↓H␈↓has the functional equation

␈↓ ↓H␈↓37)␈↓ α8 ␈↓↓∀x.(f2 x = (f2 x).␈↓NIL␈↓↓)␈↓.

␈↓ ↓H␈↓from which ␈↓↓∀x.¬issexp f2(x)␈↓ can be proved by induction.

␈↓ ↓H␈↓␈↓ α_In␈α⊃order␈α⊂to␈α⊃characterize␈α⊃recursive␈α⊂programs,␈α⊃we␈α⊃need␈α⊂some␈α⊃way␈α⊃of␈α⊂asking␈α⊃for␈α⊃the␈α⊂least
␈↓ ↓H␈↓defined solution of the functional equation.

␈↓ ↓H␈↓␈↓ α_Suppose the program is
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 99


␈↓ ↓H␈↓38)␈↓ α8 ␈↓↓f x ← ␈↓	t␈↓↓[f](x)␈↓

␈↓ ↓H␈↓yielding the functional equation

␈↓ ↓H␈↓39)␈↓ α8 ␈↓↓∀x.(f x = ␈↓	t␈↓↓[f](x)␈↓.

␈↓ ↓H␈↓The ␈↓↓minimization schema␈↓ is then

␈↓ ↓H␈↓40)␈↓ α8 ␈↓↓∀x.(isD ␈↓	t␈↓↓[␈↓	f␈↓↓](x) ⊃ ␈↓	f␈↓↓ x = ␈↓	t␈↓↓[␈↓	f␈↓↓](x)) ⊃ ∀x.(isD f x ⊃ ␈↓	f␈↓↓ x = f x)␈↓,

␈↓ ↓H␈↓where the predicate ␈↓↓isD␈↓ asserts that its argument is in the domain ␈↓↓D␈↓.

␈↓ ↓H␈↓␈↓ α_In the ␈↓↓subst␈↓ example, the schema is

␈↓ ↓H␈↓41)␈↓ α8␈α⊂␈↓↓∀x␈α⊂y␈α⊂z.(issexp␈α⊂(␈↓αif␈↓↓␈α⊂␈↓αat␈↓↓␈α∂z␈α⊂␈↓αthen␈↓↓␈α⊂(␈↓αif␈↓↓␈α⊂z␈α⊂=␈α⊂y␈α⊂␈↓αthen␈↓↓␈α∂x␈α⊂␈↓αelse␈↓↓␈α⊂z)␈α⊂␈↓αelse␈↓↓␈α⊂␈↓	f␈↓↓(x,y,␈↓αa␈↓↓␈α⊂z).␈↓	f␈↓↓(x,y,␈↓αd␈↓↓␈α⊂z))␈α∂⊃
␈↓ ↓H␈↓↓(␈↓	f␈↓↓(x,y,z)␈α∞=␈α∞␈↓αif␈↓↓␈α∞␈↓αat␈↓↓␈α∞z␈α
␈↓αthen␈↓↓␈α∞(␈↓αif␈↓↓␈α∞z␈α∞=␈α∞y␈α
␈↓αthen␈↓↓␈α∞x␈α∞␈↓αelse␈↓↓␈α∞z)␈α∞␈↓αelse␈↓↓␈α
␈↓	f␈↓↓(x,y,␈↓αa␈↓↓␈α∞z).␈↓	f␈↓↓(x,y,␈↓αd␈↓↓␈α∞z)))␈α∞⊃␈α∞∀x␈α∞y␈α
z.(issexp
␈↓ ↓H␈↓↓subst(x,y,z) ⊃ ␈↓	f␈↓↓(x,y,z) = subst(x,y,z))␈↓.

␈↓ ↓H␈↓␈↓ α_In␈αthe␈αschema␈α␈↓	f␈↓␈αis␈αa␈αfree␈αfunction␈αvariable␈αof␈αthe␈αappropriate␈αnumber␈αof␈αarguments.␈α The
␈↓ ↓H␈↓schema is just a translation into first order logic of Park's (1970) theorem

␈↓ ↓H␈↓42)␈↓ α8 ␈↓↓␈↓	f␈↓↓ ␈↓πd␈↓↓ ␈↓	t␈↓↓[␈↓	f␈↓↓] ⊃ ␈↓	f␈↓↓ ␈↓πd␈↓↓ Y[␈↓	t␈↓↓]␈↓.

␈↓ ↓H␈↓␈↓ α_The␈α
simplest␈α
application␈α
of␈αthe␈α
schema␈α
is␈α
to␈αshow␈α
that␈α
the␈α
␈↓↓f1␈↓␈α
defined␈αby␈α
(34)␈α
is␈α
never␈αan␈α
S-
␈↓ ↓H␈↓expression.  The schema becomes

␈↓ ↓H␈↓43)␈↓ α8 ␈↓↓∀x.(issexp ␈↓	f␈↓↓ x ⊃ ␈↓	f␈↓↓ x = ␈↓	f␈↓↓ x) ⊃ ∀x.(issexp f1 x ⊃ ␈↓	f␈↓↓ x = f1 x)␈↓,

␈↓ ↓H␈↓and we take

␈↓ ↓H␈↓44)␈↓ α8 ␈↓↓␈↓	f␈↓↓ x = ␈↓	w␈↓↓␈↓.

␈↓ ↓H␈↓The␈αleft␈αside␈αof␈α(43)␈αis␈αidentically␈αtrue,␈αand,␈αremembering␈αthat␈α␈↓	w␈↓␈αis␈αnot␈αan␈αS-expression,␈αthe␈αright
␈↓ ↓H␈↓side tells us that ␈↓↓f1 x␈↓ is never an S-expression.

␈↓ ↓H␈↓␈↓ α_The␈αminimization␈αschema␈αcan␈αsometimes␈αbe␈αused␈αto␈αshow␈αpartial␈αcorrectness.␈α For␈αexample,
␈↓ ↓H␈↓the well known 91-function is defined by the recursive program over the integers

␈↓ ↓H␈↓45)␈↓ α8 ␈↓↓f91 x ← ␈↓αif␈↓↓ x > 100 ␈↓αthen␈↓↓ x - 10 ␈↓αelse␈↓↓ f91 f91(x + 11)␈↓.

␈↓ ↓H␈↓The goal is to show that

␈↓ ↓H␈↓46)␈↓ α8 ␈↓↓∀x.(f91 x = ␈↓αif␈↓↓ x > 100 ␈↓αthen␈↓↓ x - 10 ␈↓αelse␈↓↓ 91␈↓.

␈↓ ↓H␈↓We apply the minimization schema with

␈↓ ↓H␈↓47)␈↓ α8 ␈↓↓␈↓	f␈↓↓ x ← ␈↓αif␈↓↓ x > 100 ␈↓αthen␈↓↓ x - 10 ␈↓αelse␈↓↓ 91␈↓,

␈↓ ↓H␈↓and␈α
it␈αcan␈α
be␈α
shown␈αby␈α
an␈α
explicit␈αcalculation␈α
without␈α
induction␈αthat␈α
the␈α
premiss␈αof␈α
the␈αschema␈α
is
␈↓ ↓H␈↓satisfied, and this shows that ␈↓↓f91,␈↓ whenever defined has the desired value.
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ *10


␈↓ ↓H␈↓␈↓ α_The␈α
method␈α
of␈α
recursion␈α
induction␈α
(McCarthy␈α1963)␈α
is␈α
also␈α
an␈α
immediate␈α
application␈αof␈α
the
␈↓ ↓H␈↓minimization␈α
schema.␈α
 If␈α
we␈α
show␈α
that␈α
two␈αfunctions␈α
satisfy␈α
the␈α
schema␈α
of␈α
a␈α
recursive␈αprogram,
␈↓ ↓H␈↓we␈α
show␈α
that␈αthey␈α
both␈α
equal␈α
the␈αfunction␈α
computed␈α
by␈α
the␈αprogram␈α
on␈α
whereever␈α
the␈αfunction␈α
is
␈↓ ↓H␈↓defined.

␈↓ ↓H␈↓␈↓ α_The␈α
utility␈α
of␈α
the␈α
minimization␈αschema␈α
for␈α
proving␈α
partial␈α
correctness␈α
or␈αnon-termination
␈↓ ↓H␈↓depends␈α∂on␈α∂our␈α∞ability␈α∂to␈α∂name␈α∂suitable␈α∞comparison␈α∂functions.␈α∂ f1␈α∞and␈α∂f91␈α∂were␈α∂easily␈α∞treated,
␈↓ ↓H␈↓because␈α⊃the␈α⊃necessary␈α⊃comparison␈α⊃functions␈α⊃could␈α⊃be␈α⊃given␈α⊃explicitly␈α⊃without␈α⊃recursion.␈α⊂ Any
␈↓ ↓H␈↓extension␈αof␈αthe␈αlanguage␈αthat␈αprovides␈αnew␈αtools␈αfor␈αnaming␈αcomparison␈αfunctions,␈αe.g.␈αgoing␈αto
␈↓ ↓H␈↓higher order logic, will improve our ability to use the schema in proofs.

␈↓ ↓H␈↓␈↓ α_(40)␈α∂can␈α∞be␈α∂regarded␈α∞as␈α∂an␈α∞axiom␈α∂schema␈α∞involving␈α∂a␈α∞second␈α∂order␈α∞function␈α∂variable␈α∞␈↓	t␈↓.
␈↓ ↓H␈↓What␈αcan␈α
be␈αsubstituted␈α
for␈α␈↓	t␈↓␈α
is␈αa␈α quantifier␈α
free␈αλ-expression␈α
in␈αa␈α
first␈αorder␈αfunction␈α
variable.
␈↓ ↓H␈↓It␈α
may␈α
be␈α
interesting␈α
to␈α
study␈α
the␈α
sets␈α
of␈α
first␈α
order␈α
sentences␈α
that␈α
can␈α
be␈α
generated␈α
by␈αsuch␈α
second
␈↓ ↓H␈↓order␈αsentence␈αschemata.␈α Presumably,␈αsets␈αof␈αsentences␈αcan␈αbe␈αgenerated␈αin␈αthis␈αway␈αthat␈αcannnot
␈↓ ↓H␈↓be generated by schemata with only first order function variables.



␈↓ ↓H␈↓α3. Proof Methods as Axiom Schemata

␈↓ ↓H␈↓␈↓ α_Representing␈α
recursive␈α
definitions␈α
in␈αfirst␈α
order␈α
logic␈α
permits␈αus␈α
to␈α
express␈α
some␈αwell␈α
known
␈↓ ↓H␈↓methods for proving partial correctness as axiom schemata of first order logic.

␈↓ ↓H␈↓␈↓ α_For example, suppose we want to prove that if the input ␈↓↓x␈↓ of a function ␈↓↓f␈↓ defined by

␈↓ ↓H␈↓48)␈↓ α8  ␈↓↓f x ← ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ f h x␈↓

␈↓ ↓H␈↓satisfies␈α␈↓↓␈↓	F␈↓↓(x)␈↓,␈αthen␈αif␈αthe␈αfunction␈αterminates,␈αthe␈αoutput␈α␈↓↓f(x)␈↓␈αwill␈αsatisfy␈α␈↓	Y␈↓↓(x,f(x))␈↓.␈α We␈αappeal␈αto
␈↓ ↓H␈↓the following ␈↓↓axiom schema of inductive assertions␈↓:

␈↓ ↓H␈↓49)␈↓ α8  ␈↓↓∀x.(␈↓	F␈↓↓(x) ⊃ q(x,x)) ∧ ∀x y.(q(x,y) ⊃ ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ ␈↓	Y␈↓↓(x,y) ␈↓αelse␈↓↓ q(x,␈↓π ␈↓↓h y))
␈↓ ↓H␈↓↓                ⊃ ∀x.(␈↓	F␈↓↓(x) ∧ isD f x ⊃ ␈↓	Y␈↓↓(x,f x))␈↓


␈↓ ↓H␈↓where␈α␈↓↓isD␈α
f␈αx␈↓␈α
is␈αthe␈α
assertion␈αthat␈α
␈↓↓f(x)␈↓␈αis␈α
in␈αthe␈α
nominal␈αrange␈α
of␈αthe␈α
function␈αdefinition,␈α
i.e.␈αis␈α
an
␈↓ ↓H␈↓integer␈α∞or␈α
an␈α∞S-expression␈α∞as␈α
the␈α∞case␈α
may␈α∞be,␈α∞and␈α
asserts␈α∞that␈α
the␈α∞computation␈α∞terminates.␈α
 In
␈↓ ↓H␈↓order␈α⊂to␈α⊂use␈α⊂the␈α∂schema,␈α⊂we␈α⊂must␈α⊂invent␈α∂a␈α⊂suitable␈α⊂predicate␈α⊂␈↓↓q(x,y)␈↓,␈α∂and␈α⊂this␈α⊂is␈α⊂precisely␈α∂the
␈↓ ↓H␈↓method␈αof␈αinductive␈αassertions.␈α The␈αschema␈αis␈αvalid␈αfor␈αall␈αpredicates␈α␈↓	F␈↓,␈α␈↓	Y␈↓,␈αand␈α␈↓↓q␈↓,␈αand␈αa␈αsimilar
␈↓ ↓H␈↓schema can be written for any collection of mutually recursive definitions that is iterative.

␈↓ ↓H␈↓␈↓ α_The␈α∂method␈α∂of␈α∞␈↓↓subgoal␈α∂induction␈↓␈α∂for␈α∞recursive␈α∂programs␈α∂was␈α∞introduced␈α∂in␈α∂(Manna␈α∞and
␈↓ ↓H␈↓Pnueli␈α1970),␈αbut␈αthey␈αdidn't␈αgive␈αit␈αa␈αname.␈α Morris␈αand␈αWegbreit␈α(1977)␈αname␈αit,␈αextend␈αit,␈αand
␈↓ ↓H␈↓apply␈αit␈α
to␈αAlgol-like␈α
programs.␈α Unlike␈α
␈↓↓inductive␈αassertions␈↓,␈α
it␈αisn't␈α
limited␈αto␈αiterative␈α
definitions.
␈↓ ↓H␈↓Thus, for the recursive program

␈↓ ↓H␈↓50)␈↓ α8  ␈↓↓f␈↓β5␈↓↓ x ← ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ h x ␈↓αelse␈↓↓ g1 f␈↓β5␈↓↓ g2 x␈↓,

␈↓ ↓H␈↓where ␈↓↓p␈↓ is assumed total, we have
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ *11


␈↓ ↓H␈↓51)␈↓ α8  ␈↓↓∀x.(p x ⊃ q(x,h x)) ∧ ∀x z.(¬p(x) ∧ q(g2 x,z) ⊃ q(x,g1 z)) ∧ ∀x.(␈↓	F␈↓↓(x) ∧ q(x,z) ⊃ ␈↓	Y␈↓↓(x,z))
␈↓ ↓H␈↓↓                ⊃ ∀x.(␈↓	F␈↓↓(x) ∧ isD(f(x)) ⊃ ␈↓	Y␈↓↓(x,f(x)))␈↓

␈↓ ↓H␈↓␈↓ α_We␈α∞can␈α∞express␈α∞these␈α∞methods␈α∞as␈α∂axiom␈α∞schemata,␈α∞because␈α∞we␈α∞have␈α∞the␈α∞predicate␈α∂␈↓↓isD␈↓␈α∞to
␈↓ ↓H␈↓express␈α∞termination.␈α∞ The␈α∞minimization␈α∞schema␈α∞itself␈α∞can␈α∞be␈α∞proved␈α∞by␈α∞subgoal␈α∞induction.␈α
 We
␈↓ ↓H␈↓need only take ␈↓↓␈↓	F␈↓↓(x) ≡ ␈↓αtrue␈↓ and ␈↓	Y␈↓↓(x,y) ≡ (y = ␈↓	f␈↓↓(x))␈↓ and ␈↓↓q(x,y) ≡ (y = ␈↓	f␈↓↓(x))␈↓.

␈↓ ↓H␈↓␈↓ α_General␈α
rules␈αfor␈α
going␈αfrom␈α
a␈αrecursive␈α
program␈α
to␈αwhat␈α
amounts␈αto␈α
the␈αsubgoal␈α
induction
␈↓ ↓H␈↓schema␈α
are␈α
given␈α
in␈α
(Manna␈α
and␈α
Pnueli␈α
1970)␈α
and␈α
(Morris␈α
and␈α
Wegbreit␈α
1977);␈α
we␈α
need␈α
only␈α
add
␈↓ ↓H␈↓a␈α⊃conclusion␈α⊃involving␈α⊃the␈α⊃␈↓↓isD␈↓␈α⊂predicate␈α⊃to␈α⊃the␈α⊃Manna's␈α⊃and␈α⊂Pnueli␈α⊃formula␈α⊃␈↓↓W␈↓βP␈↓.␈α⊃ It␈α⊃isn't␈α⊂a
␈↓ ↓H␈↓schema in ␈↓	t␈↓ in the form they give.

␈↓ ↓H␈↓␈↓ α_However,␈α∞we␈α
can␈α∞characterize␈α
subgoal␈α∞induction␈α
as␈α∞an␈α
axiom␈α∞schema.␈α
 Namely,␈α∞we␈α
define
␈↓ ↓H␈↓␈↓	t␈↓↓'[q]␈↓ as an extension of ␈↓	t␈↓ mapping relations into relations.  Thus if

␈↓ ↓H␈↓52)␈↓ α8  ␈↓↓␈↓	t␈↓↓[f](x) = ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ h x ␈↓αelse␈↓↓ g1 f g2 x␈↓,

␈↓ ↓H␈↓we have

␈↓ ↓H␈↓53)␈↓ α8  ␈↓↓␈↓	t␈↓↓'[q](x,y) ≡ ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ (y = h x) ␈↓αelse␈↓↓ ∃z.(q(g2 x,z) ∧ y = g1 z)␈↓.

␈↓ ↓H␈↓In general we have

␈↓ ↓H␈↓54)␈↓ α8  ␈↓↓∀xy.(␈↓	t␈↓↓'[q](x,y) ⊃ q(x,y)) ⊃ ∀x.(isD f x ⊃ q(x,f x))␈↓,

␈↓ ↓H␈↓from␈α
which␈α
the␈α
subgoal␈α∞induction␈α
rule␈α
follows␈α
immediately␈α
given␈α∞the␈α
properties␈α
of␈α
␈↓	F␈↓␈α
and␈α∞␈↓	Y␈↓.␈α
 I
␈↓ ↓H␈↓am indebted to Wolfgang Polak (oral communication) for help in elucidating this relationship.

␈↓ ↓H␈↓␈↓αWARNING␈↓:␈αThe␈αrest␈α
of␈αthis␈αsection␈α
is␈αstill␈αsomewhat␈α
conjectural␈αand␈αis␈α
subject␈αto␈αchange.␈α
 There
␈↓ ↓H␈↓may be bugs.

␈↓ ↓H␈↓␈↓ α_The␈αextension␈α
␈↓↓␈↓	t␈↓↓'[q]␈↓␈αcan␈α
be␈αdetermined␈α
as␈αfollows:␈α
Introduce␈αinto␈α
the␈αlogic␈α
the␈αnotion␈α
of␈αa
␈↓ ↓H␈↓␈↓↓multi-term␈↓␈α
which␈αis␈α
formed␈αin␈α
the␈αsame␈α
way␈α
as␈αa␈α
term␈αbut␈α
allows␈αrelations␈α
written␈α
as␈αfunctions.
␈↓ ↓H␈↓For␈α∀the␈α∀present␈α∃we␈α∀won't␈α∀interpret␈α∃them␈α∀but␈α∀merely␈α∀give␈α∃rules␈α∀for␈α∀introducing␈α∃them␈α∀and
␈↓ ↓H␈↓subsequently␈α
eliminating␈αthem␈α
again␈α
to␈αget␈α
an␈α
ordinary␈αformula.␈α
 Thus␈α
we␈αwill␈α
write␈α
␈↓↓q<e>␈↓␈αwhere␈α
␈↓↓e␈↓
␈↓ ↓H␈↓is␈αany␈αterm␈αor␈αmulti-term.␈α We␈αthen␈αform␈α
␈↓↓␈↓	t␈↓↓'[q]␈↓␈αexactly␈αin␈αthe␈αsame␈αway␈α␈↓↓␈↓	t␈↓↓[f]␈↓␈αwas␈α
formed.␈α Thus
␈↓ ↓H␈↓for the 91-function we have

␈↓ ↓H␈↓55)␈↓ α8  ␈↓↓␈↓	t␈↓↓'[q](x) = ␈↓αif␈↓↓ x>100 ␈↓αthen␈↓↓ x-10 ␈↓αelse␈↓↓ q<q<x+11>>␈↓.

␈↓ ↓H␈↓The␈α⊃pointy␈α⊃brackets␈α⊃indicate␈α⊃that␈α⊃we␈α⊃are␈α⊃"applying"␈α⊃a␈α⊃relation.␈α⊃ We␈α⊃now␈α⊃evaluate␈α⊂␈↓↓␈↓	t␈↓↓'[q](x,y)␈↓
␈↓ ↓H␈↓formally as follows:

␈↓ ↓H␈↓56)␈↓ α8  ␈↓↓␈↓	t␈↓↓'[q](x,y)   ≡ (␈↓αif␈↓↓ x>100 ␈↓αthen␈↓↓ x-10 ␈↓αelse␈↓↓ q<q<x+11>>)(y)

␈↓ ↓H␈↓↓                        ≡ ␈↓αif␈↓↓ x>100 ␈↓αthen␈↓↓ y = x-10 ␈↓αelse␈↓↓ q(q<x+11>,y)

␈↓ ↓H␈↓↓                        ≡ ␈↓αif␈↓↓ x>100 ␈↓αthen␈↓↓ y = x-10 ␈↓αelse␈↓↓ ∃z.(q(x+11,z) ∧ q(z,y))␈↓.
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ *12


␈↓ ↓H␈↓This␈α⊂last␈α⊂formula␈α∂has␈α⊂no␈α⊂pointy␈α∂brackets␈α⊂and␈α⊂is␈α∂just␈α⊂the␈α⊂formula␈α∂that␈α⊂would␈α⊂be␈α⊂obtained␈α∂by
␈↓ ↓H␈↓Manna and Pnueli or Morris and Wegbreit.  The rules are as follows:

␈↓ ↓H␈↓␈↓ α_(i)␈α∂␈↓↓␈↓	t␈↓↓'[q](x)␈↓␈α∂is␈α∂just␈α∂like␈α∂␈↓↓␈↓	t␈↓↓[f](x)␈↓␈α∂except␈α∂that␈α∂␈↓↓q␈↓␈α∂replaces␈α∂␈↓↓f␈↓␈α∂and␈α∂takes␈α∂its␈α∂arguments␈α∂in␈α∞pointy
␈↓ ↓H␈↓brackets.

␈↓ ↓H␈↓␈↓ α_(ii) an ordinary term ␈↓↓e␈↓ applied to ␈↓↓y␈↓ becomes ␈↓↓y = e␈↓.

␈↓ ↓H␈↓␈↓ α_(ii) ␈↓↓q<e>(y)␈↓ becomes ␈↓↓q(e,y)␈↓.

␈↓ ↓H␈↓␈↓ α_(ii)␈α∪␈↓↓P(q<e>)␈↓␈α∪becomes␈α∪␈↓↓∃z.q(e,z) ∧ P(z)␈↓␈α∪when␈α∩␈↓↓P(q<e>)␈↓␈α∪occurs␈α∪positively␈α∪in␈α∪␈↓↓␈↓	t␈↓↓'[q](x,y)␈↓␈α∩and
␈↓ ↓H␈↓becomes␈α⊂␈↓↓∀z.q(e,z) ⊃ P(z)␈↓␈α⊂when␈α⊂the␈α⊂occurrence␈α⊂is␈α⊂negatve.␈α⊂ It␈α⊂is␈α⊂not␈α⊂evident␈α⊃what␈α⊂independent
␈↓ ↓H␈↓semantics should be given to multi-terms.




␈↓ ↓H␈↓α4. Representations Using Finite Approximations.

␈↓ ↓H␈↓␈↓ α_Our␈αsecond␈αapproach␈αto␈αrepresenting␈αrecursive␈αprograms␈αby␈αfirst␈αorder␈αformulas␈αgoes␈αback
␈↓ ↓H␈↓to␈α⊂G␈↓
:␈↓odel␈α⊂(1931,␈α∂1934)␈α⊂who␈α⊂showed␈α∂that␈α⊂primitive␈α⊂recursive␈α∂functions␈α⊂could␈α⊂be␈α⊂so␈α∂represented.
␈↓ ↓H␈↓(Our knowledge of G␈↓
:␈↓odel's work comes from (Kleene 1951)).

␈↓ ↓H␈↓␈↓ α_Kleene␈α(1951)␈α
calls␈αa␈αfunction␈α
␈↓↓f␈↓␈α␈↓↓representable␈↓␈αif␈α
there␈αis␈αan␈α
arithmetic␈αformula␈α␈↓↓A␈↓␈α
with␈αfree
␈↓ ↓H␈↓variables ␈↓↓x␈↓ and ␈↓↓y␈↓ such that

␈↓ ↓H␈↓1)␈↓ α8  ␈↓↓∀x y.((y = f(x)) ≡ A)␈↓,

␈↓ ↓H␈↓where␈αan␈αarithmetic␈αformula␈αis␈αbuilt␈αup␈αfrom␈αinteger␈αconstants␈αand␈αvariables␈αusing␈αonly␈αaddition,
␈↓ ↓H␈↓multiplication␈αand␈αbounded␈α
quantification.␈α Kleene␈αshowed␈αthat␈α
all␈αpartial␈αrecursive␈αfunctions␈α
are
␈↓ ↓H␈↓representable.␈α The␈α
proof␈αinvolves␈αG␈↓
:␈↓odel␈α
numbering␈αpossible␈α
computation␈αsequences␈αand␈α
showing
␈↓ ↓H␈↓that␈α
the␈α∞relation␈α
between␈α
sequences␈α∞and␈α
their␈α
elements␈α∞and␈α
the␈α
steps␈α∞of␈α
the␈α
computation␈α∞are␈α
all
␈↓ ↓H␈↓representable.

␈↓ ↓H␈↓␈↓ α_In␈αLisp␈αless␈αmachinery␈α
has␈αto␈αbe␈αbuilt␈α
up,␈αbecause␈αsequences␈αare␈α
Lisp␈αdata,␈αand␈αthe␈α
relation
␈↓ ↓H␈↓between␈α∞a␈α∞sequence␈α∞and␈α∞its␈α∞elements␈α∞is␈α∞given␈α∞by␈α∞basic␈α∞Lisp␈α∞functions␈α∞and␈α∞by␈α∞the␈α∞␈↓↓subexpression
␈↓ ↓H␈↓↓relation␈↓ defined by

␈↓ ↓H␈↓2)␈↓ α8  ␈↓↓x subexp y ← (x = y) ∨ ¬␈↓αat␈↓↓ y ∧ [x subexp ␈↓αa␈↓↓ y ∨ x subexp ␈↓αd␈↓↓ y]␈↓.

␈↓ ↓H␈↓␈↓ α_␈↓↓subexp␈↓␈α
is␈α
the␈α
only␈α
recursive␈α
definition␈α
we␈α∞shall␈α
require.␈α
 Since␈α
it␈α
is␈α
total,␈α
we␈α
only␈α∞need␈α
its
␈↓ ↓H␈↓functional equation to represent it in first order logic.  The functional equation is

␈↓ ↓H␈↓L17:    ␈↓↓∀x y.(x subexp y ≡ (x=y) ∨ ¬␈↓αat␈↓↓ y ∧ (x subexp ␈↓αa␈↓↓ y ∨ x subexp ␈↓αd␈↓↓ y))␈↓,

␈↓ ↓H␈↓␈↓ α_The␈α⊃axiom␈α⊃system␈α⊃consisting␈α⊂of␈α⊃L1-L17,␈α⊃B1-B12,␈α⊃and␈α⊂the␈α⊃sentences␈α⊃resulting␈α⊃from␈α⊂the
␈↓ ↓H␈↓schemata LS1 and LS2 will be called the axiom system Lisp1.

␈↓ ↓H␈↓␈↓ α_Starting␈αwith␈α␈↓↓subexp␈↓␈αand␈αthe␈αbasic␈αLisp␈αfunctions␈αand␈αpredicates␈αwe␈αwill␈αdefine␈αthree␈αother
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ *13


␈↓ ↓H␈↓Lisp␈α⊃predicates␈α⊂without␈α⊃recursion.␈α⊂ By␈α⊃␈↓↓u istail v␈↓␈α⊂we␈α⊃mean␈α⊂that␈α⊃␈↓↓u␈↓␈α⊂can␈α⊃be␈α⊂obtained␈α⊃from␈α⊃␈↓↓v␈↓␈α⊂by
␈↓ ↓H␈↓repeated␈α␈↓↓cdr␈↓s.␈α Thus␈αthe␈αtails␈αof␈α(A␈α
B␈αC␈αD)␈αare␈α(A␈αB␈αC␈αD),␈α
(B␈αC␈αD),␈α(C␈αD),␈α(D)␈αand␈α
NIL.␈α The
␈↓ ↓H␈↓natural recursive definition of ␈↓↓istail␈↓ is

␈↓ ↓H␈↓3)␈↓ α8 ␈↓↓u istail v ← (u = v) ∨ (¬␈↓αn␈↓↓ v ∧ u istail ␈↓αd␈↓↓ v)␈↓

␈↓ ↓H␈↓which according to the previous sections would lead to the first order formula

␈↓ ↓H␈↓4)␈↓ α8 ␈↓↓∀u v.(u istail v ≡ (u = v) ∨ (¬␈↓αn␈↓↓ v ∧ u istail ␈↓αd␈↓↓ v))␈↓,

␈↓ ↓H␈↓but␈α
(4)␈α
is␈α
still␈α
an␈αimplicit␈α
definition␈α
of␈α
␈↓↓istail␈↓,␈α
because␈αthe␈α
function␈α
being␈α
defined␈α
occurs␈α
on␈αboth
␈↓ ↓H␈↓sides of the equivalence sign.  A suitable explicit definition is

␈↓ ↓H␈↓5)␈↓ α8  ␈↓↓∀u v.(u istail v ≡ u subexp v ∧ ∀x.(u subexp x ∧ x subexp v ⊃ x = u ∨ u subexp ␈↓αd␈↓↓ x))␈↓.

␈↓ ↓H␈↓Next we shall define membership in a list.  We have

␈↓ ↓H␈↓6)␈↓ α8  ␈↓↓∀x v.(x ε v ≡ ∃u.(u istail v ∧ x = ␈↓αa␈↓↓ u))␈↓.

␈↓ ↓H␈↓Now we define an ␈↓↓a-list␈↓ - a familiar Lisp concept.  We have

␈↓ ↓H␈↓7)␈↓ α8␈α
 ␈↓↓∀w.(isalist␈αw␈α
≡␈α
∀x.(x␈αε␈α
w␈α
⊃␈α¬␈↓αat␈↓↓␈α
x)␈α
∧␈α∀u1␈α
u2.(u1␈αistail␈α
w␈α
∧␈αu2␈α
istail␈α
w␈α∧␈α
␈↓αaa␈↓↓␈α
u1␈α=␈α
␈↓αaa␈↓↓␈αu2␈α
⊃
␈↓ ↓H␈↓↓u1 = u2))␈↓.

␈↓ ↓H␈↓Thus␈α∞an␈α
␈↓↓a-list␈↓␈α∞is␈α∞a␈α
list␈α∞of␈α
pairs␈α∞such␈α∞that␈α
no␈α∞S-expression␈α
is␈α∞the␈α∞first␈α
element␈α∞of␈α∞two␈α
different
␈↓ ↓H␈↓pairs.␈α⊃ Therefore,␈α⊃a-lists␈α⊃are␈α⊃suitable␈α⊃for␈α⊂representing␈α⊃finite␈α⊃lists␈α⊃of␈α⊃argument-value␈α⊃pairs␈α⊂for
␈↓ ↓H␈↓partial functions.

␈↓ ↓H␈↓␈↓ α_Finally,␈α
we␈α
need␈α
the␈α
familiar␈α
Lisp␈α
function␈α
␈↓↓assoc␈↓␈α
that␈α
is␈α
used␈α
for␈α
looking␈α
up␈α
atoms␈α
on␈α␈↓↓a-
␈↓ ↓H␈↓↓lists␈↓.  Its familiar recursive definition is

␈↓ ↓H␈↓8)␈↓ α8  ␈↓↓assoc(x,w) ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ w ␈↓αthen␈↓↓ ␈↓NIL␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ x = ␈↓αaa␈↓↓ w ␈↓αthen␈↓↓ ␈↓αa␈↓↓ w ␈↓αelse␈↓↓ assoc(x,␈↓αd␈↓↓ w)␈↓,

␈↓ ↓H␈↓but it can be represented by

␈↓ ↓H␈↓9)␈↓ α8  ␈↓↓∀w x y.(x.y = assoc(x,w) ≡ ∃w1.(w1 istail w ∧ x.y = ␈↓αa␈↓↓ w1) ∨ assoc(x,w) = ␈↓NIL␈↓↓)␈↓.

␈↓ ↓H␈↓␈↓ α_Now let ␈↓↓f␈↓ be an arbitrary recursive program defined by

␈↓ ↓H␈↓10)␈↓ α8  ␈↓↓f x ← ␈↓	t␈↓↓[f](x)␈↓

␈↓ ↓H␈↓for␈αsome␈αcontinuous␈αfunctional␈α␈↓	t␈↓.␈α In␈αorder␈αto␈αemphasize␈αthe␈αparallel␈αbetween␈αa␈αpartial␈αfunction␈α
␈↓↓f␈↓
␈↓ ↓H␈↓and an ␈↓↓a-list␈↓ used as a finite approximation, we define

␈↓ ↓H␈↓11)␈↓ α8 ␈↓	t␈↓↓'(w)(x) = ␈↓	t␈↓↓[λz.␈↓αif␈↓↓ ␈↓αn␈↓↓ assoc(z,w) ␈↓αthen␈↓↓ ␈↓	w␈↓↓ ␈↓αelse␈↓↓ ␈↓αd␈↓↓ assoc(z,w)](x)␈↓.

␈↓ ↓H␈↓Thus␈α␈↓	t␈↓'␈αis␈αlike␈α␈↓	t␈↓␈αexcept␈αthat␈αwhenever␈α␈↓	t␈↓␈αevaluates␈αits␈αfunctional␈αargument␈α␈↓↓f␈↓␈αat␈αsome␈αvalue␈α␈↓↓z,␈↓␈α␈↓	t␈↓'
␈↓ ↓H␈↓looks up ␈↓↓z␈↓ on the a-list ␈↓↓w.␈↓

␈↓ ↓H␈↓␈↓ α_With this preparation we can write
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ *14


␈↓ ↓H␈↓12)␈↓ α8␈α
 ␈↓↓∀x␈α
y.(y␈α
=␈α
f(x)␈α
≡␈α
∃w.(x.y␈α∞=␈α
␈↓αa␈↓↓␈α
w␈α
∧␈α
∀x1␈α
y1␈α
w1.(w1␈α
istail␈α∞w␈α
∧␈α
x1.y1␈α
=␈α
␈↓αa␈↓↓␈α
w1␈α
⊃␈α
y1␈α∞=␈α
␈↓	t␈↓↓'[␈↓αd␈↓↓
␈↓ ↓H␈↓↓w1](x1))) ∨ f(x) = ␈↓	w␈↓↓)␈↓.

␈↓ ↓H␈↓␈↓ α_The␈α∞essence␈α
of␈α∞this␈α
formula␈α∞is␈α
simple.␈α∞ ␈↓↓w␈↓␈α
is␈α∞an␈α
a-list␈α∞containing␈α
all␈α∞argument-value␈α
pairs
␈↓ ↓H␈↓that␈α⊂arise␈α⊂in␈α⊂the␈α⊂evaluation␈α∂of␈α⊂␈↓↓f(x).␈↓␈α⊂We␈α⊂require␈α⊂that␈α⊂if␈α∂␈↓↓x␈↓␈α⊂occurs␈α⊂somewhere␈α⊂on␈α⊂␈↓↓w,␈↓␈α⊂the␈α∂pairs
␈↓ ↓H␈↓involved␈α∞in␈α∞the␈α∞evaluation␈α∂of␈α∞␈↓↓f(x)␈↓␈α∞occur␈α∞further␈α∂on␈α∞in␈α∞the␈α∞a-list␈α∂␈↓↓w.␈↓␈α∞ This␈α∞is␈α∞to␈α∂avoid␈α∞allowing
␈↓ ↓H␈↓circular recursions.  If there is no such a-list, then ␈↓↓f(x) = ␈↓	w␈↓.

␈↓ ↓H␈↓␈↓ α_If␈α
the␈αlogic␈α
has␈α
a␈αdescription␈α
operator␈α
␈↓	i␈↓,␈αwhere␈α
␈↓	i␈↓↓␈α
x.P(x)␈↓␈αstands␈α
for␈α
the␈α"the␈α
unique␈α
␈↓↓x␈↓␈αsuch
␈↓ ↓H␈↓that ␈↓↓P(x)␈↓ if there is such a unique ␈↓↓x␈↓ and otherwise ␈↓	w␈↓", then (12) can be written

␈↓ ↓H␈↓13)␈↓ α8␈α∂␈↓↓∀x.(f(x)␈α∂=␈α∂␈↓	i␈↓↓␈α∂y.∃w.(x.y␈α∂=␈α∂␈↓αa␈↓↓␈α∂w␈α∂∧␈α∂∀x1␈α∂y1␈α∂w1.(w1␈α∂istail␈α∂w␈α∂∧␈α∂x1.y1␈α∂=␈α∂␈↓αa␈↓↓␈α∂w1␈α∂⊃␈α∂y1␈α∂=␈α∂␈↓	t␈↓↓'[␈↓αd␈↓↓
␈↓ ↓H␈↓↓w1](x1))))␈↓.

␈↓ ↓H␈↓␈↓ α_As an example, consider the Lisp function ␈↓↓ff␈↓ defined recursively by

␈↓ ↓H␈↓14)␈↓ α8 ␈↓↓ff x ← ␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ ff ␈↓αa␈↓↓ x␈↓.

␈↓ ↓H␈↓(13) then takes the form

␈↓ ↓H␈↓15)␈↓ α8␈α
∀x.(ff␈αx␈α
=␈α
␈↓	i␈↓↓y.∃w.(x.y␈α=␈α
␈↓αa␈↓↓␈α
w␈α∧␈α
∀x1␈α
y1␈αw1.(w1␈α
istail␈αw␈α
∧␈α
x1.y1␈α=␈α
␈↓αa␈↓↓␈α
w1␈α⊃␈α
y1␈α
=␈α␈↓αif␈↓↓␈α
␈↓αat␈↓↓␈αx1␈α
␈↓αthen␈↓↓
␈↓ ↓H␈↓↓x1 ␈↓αelse␈↓↓ (␈↓αif␈↓↓ ␈↓αn␈↓↓ assoc(x1,␈↓αd␈↓↓ w1) ␈↓αthen␈↓↓ ␈↓	w␈↓↓ ␈↓αelse␈↓↓ ␈↓αd␈↓↓ assoc(x1,␈↓αd␈↓↓ w1)))))␈↓.

␈↓ ↓H␈↓␈↓ α_Suppose␈α∞we␈α∞were␈α∞computing␈α∞␈↓↓ff ((A.B).C)␈↓.␈α
 A␈α∞suitable␈α∞␈↓↓w␈↓␈α∞would␈α∞be␈α∞((((A.B).C).A)␈α
((A.B).A)
␈↓ ↓H␈↓(A.A)).

␈↓ ↓H␈↓␈↓ α_It␈α
might␈α∞be␈α
asked␈α
whether␈α∞␈↓↓subexp␈↓␈α
is␈α
necessary.␈α∞ Couldn't␈α
we␈α
represent␈α∞recursive␈α
programs
␈↓ ↓H␈↓using␈αjust␈α␈↓↓car,␈αcdr,␈αcons␈↓␈αand␈α␈↓↓atom␈↓?␈α No,␈αfor␈αthe␈αfollowing␈αreason.␈α Suppose␈αthat␈αthe␈αfunction␈α␈↓↓f␈↓␈αis
␈↓ ↓H␈↓representable using only the basic Lisp functions without ␈↓↓subexp␈↓, and consider the sentence

␈↓ ↓H␈↓16)␈↓ α8 ␈↓↓∀x.issexp f(x)␈↓,

␈↓ ↓H␈↓asserting␈αthe␈αtotality␈α
of␈α␈↓↓f.␈↓␈αUsing␈α
the␈αrepresentation,␈αwe␈α
can␈αwrite␈α(16)␈α
as␈αa␈αsentence␈αinvolving␈α
only
␈↓ ↓H␈↓the␈α
basic␈αLisp␈α
functions␈α
and␈αthe␈α
constant␈α␈↓	w␈↓.␈α
 However,␈α
as␈αis␈α
shown␈α
in␈αAppendix␈α
I,␈αthese␈α
sentences
␈↓ ↓H␈↓are␈αdecidable,␈α
and␈αtotality␈α
isn't.␈α (I'll␈α
put␈αthe␈α
proof␈αin␈α
Appendix␈αI␈α
if␈αI␈α
can␈αprove␈α
it.␈α At␈α
this␈αtime,␈α
I
␈↓ ↓H␈↓think I've almost got it).

␈↓ ↓H␈↓␈↓ α_In␈α∞case␈α∞of␈α∞functions␈α∞of␈α∞several␈α∞variables,␈α∞(12)␈α∞corresponds␈α∞to␈α∞a␈α∂call-by-value␈α∞computation
␈↓ ↓H␈↓rule␈αwhile␈αthe␈αrepresentations␈αof␈αthe␈αprevious␈αsections␈αcorrespond␈αto␈αcall-by-name␈αor␈αother␈α"safe"
␈↓ ↓H␈↓rules.␈α∞ The␈α∞difference␈α∂is␈α∞not␈α∞important,␈α∂because␈α∞of␈α∞Vuillemin's␈α∂theorem␈α∞that␈α∞any␈α∂strict␈α∞function
␈↓ ↓H␈↓may be computed either according to call-by-name or call-by-value.


␈↓ ↓H␈↓α5. Questions of Incompleteness.

␈↓ ↓H␈↓␈↓ α_Luckham,␈αPark␈αand␈αPaterson␈α(1970)␈αhave␈αshown␈αthat␈αwhether␈αa␈αprogram␈α
schema␈αdiverges
␈↓ ↓H␈↓for␈α∞every␈α∞interpretation,␈α∂whether␈α∞it␈α∞diverges␈α∞for␈α∂some␈α∞interpretation,␈α∞and␈α∞whether␈α∂two␈α∞program
␈↓ ↓H␈↓schemas␈α∀are␈α∪equivalent␈α∀are␈α∀all␈α∪not␈α∀even␈α∪partially␈α∀solvable␈α∀problems.␈α∪ Manna␈α∀(1974)␈α∀has␈α∪a
␈↓ ↓H␈↓thorough␈αdiscussion␈αof␈αthese␈αpoints.␈α In␈αview␈αof␈αthese␈αresults,␈αwhat␈αcan␈αbe␈αexpected␈αfrom␈αour␈αfirst
␈↓ ↓H␈↓order representations?
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ *15


␈↓ ↓H␈↓␈↓ α_First␈α
let␈α
us␈α
construct␈α
a␈α
Lisp␈α
computation␈α
that␈α
does␈α
not␈α
terminate,␈α
but␈α
whose␈α
non-termination
␈↓ ↓H␈↓cannot␈α
be␈α
proved␈α
from␈α
the␈αaxioms␈α
Lisp1␈α
within␈α
first␈α
order␈αlogic.␈α
 We␈α
need␈α
only␈α
program␈αa␈α
proof-
␈↓ ↓H␈↓checker␈α
for␈αfirst␈α
order␈α
logic,␈αset␈α
it␈α
to␈αgenerate␈α
all␈αpossible␈α
proofs␈α
starting␈αwith␈α
the␈α
axioms␈αLisp1,
␈↓ ↓H␈↓and␈α
stop␈α
when␈α
it␈αfinds␈α
a␈α
proof␈α
of␈α(NIL␈α
≠␈α
NIL)␈α
or␈αsome␈α
other␈α
contradiction.␈α
 Assuming␈αthe␈α
axioms
␈↓ ↓H␈↓are␈α
consistent,␈αthe␈α
program␈αwill␈α
never␈α
find␈αsuch␈α
a␈αproof␈α
and␈α
will␈αnever␈α
stop.␈α In␈α
fact,␈αproving␈α
that
␈↓ ↓H␈↓the␈α⊂program␈α⊂will␈α⊂never␈α⊂stop␈α⊂is␈α⊃precisely␈α⊂proving␈α⊂that␈α⊂the␈α⊂axioms␈α⊂are␈α⊂consistent.␈α⊃ But␈α⊂G␈↓
:␈↓odel's
␈↓ ↓H␈↓theorem␈αasserts␈αthat␈αaxiom␈αsystems␈αlike␈αLisp1␈αcannot␈αbe␈αproved␈αconsistent␈αwithin␈αthemselves.␈α All
␈↓ ↓H␈↓the␈αknown␈αcases␈αof␈αterminating␈αcomputations␈αthat␈αcan't␈αbe␈αproved␈αnot␈αto␈αterminate␈αwithin␈αPeano
␈↓ ↓H␈↓arithemtic involve such an appeal to G␈↓
:␈↓odel's theorem or similar unsolvability arguments.

␈↓ ↓H␈↓␈↓ α_We␈α
can␈α
presumably␈α
prove␈αLisp1␈α
consistent␈α
just␈α
as␈αGentzen␈α
proved␈α
arithmetic␈α
consistent␈α-␈α
at
␈↓ ↓H␈↓the␈α
price␈αof␈α
introducing␈α
a␈αnew␈α
axiom␈αschema␈α
that␈α
allows␈αinduction␈α
up␈αto␈α
the␈α
transfinite␈αordinal
␈↓ ↓H␈↓ε␈↓β0␈↓.  Proving the new system consistent would require induction up to a still higher ordinal, etc.

␈↓ ↓H␈↓␈↓ α_Since␈α∞every␈α∞recursively␈α∞defined␈α∞function␈α∞can␈α∞be␈α∞defined␈α∞explicitly,␈α∞any␈α∞sentence␈α
involving
␈↓ ↓H␈↓such␈α∂functions␈α∞can␈α∂be␈α∞replaced␈α∂by␈α∞an␈α∂equivalent␈α∞sentence␈α∂involving␈α∞only␈α∂␈↓↓subexp␈↓␈α∞and␈α∂the␈α∞basic
␈↓ ↓H␈↓Lisp␈α∞functions.␈α∞ The␈α∞theory␈α∞of␈α∞subexp␈α∞and␈α∞these␈α∞functions␈α∞has␈α∞a␈α∞standard␈α∞model,␈α∞the␈α∂usual␈α∞S-
␈↓ ↓H␈↓expressions␈α∞and␈α∞many␈α∂non-standard␈α∞models.␈α∞ We␈α∞"construct"␈α∂non-standard␈α∞models␈α∞in␈α∂the␈α∞usual
␈↓ ↓H␈↓way␈α
by␈αappealing␈α
to␈αthe␈α
theorem␈αthat␈α
if␈αevery␈α
finite␈αsubset␈α
of␈αa␈α
set␈α␈↓↓S␈↓␈α
of␈αsentences␈α
of␈α
first␈αorder
␈↓ ↓H␈↓logic␈αhas␈αa␈αmodel,␈αthen␈α␈↓↓S␈↓␈αhas␈αa␈αmodel.␈α For␈αexample,␈αtake␈α␈↓↓S␈α=␈α{␈↓NIL␈↓↓␈αsubexp␈αx,␈α␈↓(A)␈↓↓␈αsubexp␈αx,␈α␈↓(A
␈↓ ↓H␈↓A)␈↓↓␈α
subexp␈α
x,␈α
...␈↓␈α
indefinitely}.␈α
 Every␈α
finite␈α
subset␈α
of␈α
␈↓↓S␈↓␈α
has␈α
a␈α
model;␈α
we␈α
need␈α
only␈α
take␈α
␈↓↓x␈↓␈α
to␈α
be␈α
the
␈↓ ↓H␈↓longest␈αlist␈αof␈αA's␈α
occurring␈αin␈αthe␈αsentences.␈α Hence␈α
there␈αis␈αa␈αmodel␈α
of␈αthe␈αLisp␈αaxioms␈αin␈α
which
␈↓ ↓H␈↓␈↓↓x␈↓␈αhas␈αall␈αlists␈αof␈αA's␈αas␈αsubexpressions.␈α No␈αsentence␈αtrue␈αin␈αthe␈αstandard␈αmodel␈αand␈αfalse␈αin␈αsuch
␈↓ ↓H␈↓a␈α
model␈α
can␈α
be␈α
proved␈α
from␈α
the␈α
axioms.␈α
 However,␈α
it␈α
is␈α
necessary␈α
to␈α
be␈α
careful␈α
about␈αthe␈α
meaning
␈↓ ↓H␈↓of␈αtermination␈αof␈αa␈αfunction.␈α
 In␈αfact,␈αtaking␈αsuccessive␈α␈↓↓cdr␈↓s␈α
of␈αsuch␈αan␈α␈↓↓x␈↓␈αwould␈α
never␈αterminate,
␈↓ ↓H␈↓but␈α
the␈αsentence␈α
whose␈α␈↓↓standard␈α
interpretation␈↓␈αis␈α
termination␈αof␈α
the␈αcomputation␈α
is␈αprovable␈α
from
␈↓ ↓H␈↓Lisp1.

␈↓ ↓H␈↓␈↓ α_The␈α⊂practical␈α⊂question␈α∂is:␈α⊂where␈α⊂does␈α∂the␈α⊂correctness␈α⊂of␈α∂ordinary␈α⊂programs␈α⊂come␈α⊂in?␈α∂ It
␈↓ ↓H␈↓seems␈αlikely␈α
that␈αsuch␈α
statements␈αwill␈αbe␈α
provable␈αwith␈α
our␈αoriginal␈αsystem␈α
of␈αaxioms.␈α
 It␈αdoesn't
␈↓ ↓H␈↓follow␈α∞that␈α∞the␈α∞system␈α∂Lisp1␈α∞will␈α∞permit␈α∞convenient␈α∞proofs,␈α∂but␈α∞probably␈α∞it␈α∞will.␈α∂ The␈α∞heuristic
␈↓ ↓H␈↓evidence␈α
for␈α
this␈α
comes␈α
from␈α
(Cohen␈α
1965).␈α
 Cohen␈α
presents␈α
two␈α
systems␈α
of␈α
axiomatized␈α
arithmetic
␈↓ ↓H␈↓Z1␈α
and␈α
Z2.␈α
 Z1␈α∞is␈α
ordinary␈α
Peano␈α
arithmetic␈α∞with␈α
an␈α
axiom␈α
schema␈α∞of␈α
induction,␈α
and␈α
Z2␈α∞is␈α
an
␈↓ ↓H␈↓axiomatization␈α
of␈αhereditarily␈α
finite␈α
sets␈αof␈α
integers.␈α Superficially,␈α
Z2␈α
is␈αmore␈α
powerful␈α
than␈αZ1,
␈↓ ↓H␈↓but␈αbecause␈αthe␈αset␈αoperations␈αof␈αZ2␈αcan␈αbe␈αrepresented␈αin␈αZ1␈αas␈αfunctions␈αon␈αthe␈αG␈↓
:␈↓odel␈αnumbers
␈↓ ↓H␈↓of␈α⊃the␈α⊃sets,␈α∩it␈α⊃turns␈α⊃out␈α∩that␈α⊃Z1␈α⊃is␈α⊃just␈α∩as␈α⊃powerful␈α⊃once␈α∩the␈α⊃necessary␈α⊃machinery␈α∩has␈α⊃been
␈↓ ↓H␈↓established.␈α Because␈αsets␈αand␈αlists␈αare␈αthe␈αbasic␈αdata␈αof␈αLisp1,␈αand␈αsets␈αare␈αeasily␈αrepresented,␈αthe
␈↓ ↓H␈↓power␈αof␈αLisp1␈αwill␈αbe␈αapproximately␈αthat␈αof␈αZ2,␈αand␈αconvenient␈αproofs␈αof␈αcorrectness␈αstatements
␈↓ ↓H␈↓should be possible.  It would be nice to be able to express these considerations less vaguely.


␈↓ ↓H␈↓α6. References.

␈↓ ↓H␈↓␈↓αCartwright,␈αR.S.␈α(1977)␈↓:␈α
␈↓↓A␈αPractical␈αFormal␈α
Semantic␈αDefinition␈αand␈α
Verification␈αSystem␈αfor␈α
Typed
␈↓ ↓H␈↓↓Lisp␈↓, Ph.D. Thesis, Computer Science Department, Stanford University, Stanford, California.

␈↓ ↓H␈↓␈↓αCohen, Paul (1966)␈↓: ␈↓↓Set Theory and the Continuum Hypothesis␈↓, W.A. Benjamin Inc.

␈↓ ↓H␈↓␈↓αCooper,␈αD.C.␈α(1969)␈↓:␈α"Program␈αScheme␈αEquivalences␈αand␈αSecond-order␈αLogic",␈αin␈αB.␈αMeltzer␈αand
␈↓ ↓H␈↓D. Michie (eds.), ␈↓↓Machine Intelligence␈↓, Vol. 4, pp. 3-15, Edinburgh University Press, Edinburgh.
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ *16


␈↓ ↓H␈↓␈↓αKleene, S.C. (1951)␈↓: ␈↓↓Introduction to Metamathematics␈↓, Van Nostrand, New York.

␈↓ ↓H␈↓␈↓αLuckham,␈αD.C.,␈αD.M.R.Park,␈α
and␈αM.S.␈αPaterson␈α(1970)␈↓:␈α
"On␈αFormalized␈αComputer␈αPrograms",␈α
␈↓↓J.
␈↓ ↓H␈↓↓CSS␈↓, ␈↓α4␈↓(3): 220-249 (June).

␈↓ ↓H␈↓␈↓αManna,␈αZohar␈αand␈α
Amir␈αPnueli␈α(1970)␈↓:␈α
"Formalization␈αof␈αthe␈α
Properties␈αof␈αFunctional␈α
Programs",
␈↓ ↓H␈↓␈↓↓J. ACM␈↓, ␈↓α17␈↓(3): 555-569.

␈↓ ↓H␈↓␈↓αManna, Zohar (1974)␈↓: ␈↓↓Mathematical Theory of Computation␈↓, McGraw-Hill.

␈↓ ↓H␈↓␈↓αManna,␈α∀Zohar,␈α∀Stephen␈α∀Ness␈α∀and␈α∀Jean␈α∀Vuillemin␈α∀(1973)␈↓:␈α∀"Inductive␈α∀Methods␈α∀for␈α∀Proving
␈↓ ↓H␈↓Properties of Programs", ␈↓↓Comm. ACM␈↓,␈↓α16␈↓(8): 491-502 (August).

␈↓ ↓H␈↓␈↓αMorris,␈α⊂James␈α⊂H.,␈α⊂and␈α∂Ben␈α⊂Wegbreit␈α⊂(1977)␈↓:␈α⊂"Program␈α∂Verification␈α⊂by␈α⊂Subgoal␈α⊂Induction",␈α∂to
␈↓ ↓H␈↓appear.

␈↓ ↓H␈↓␈↓αPark,␈α_David␈α_(1969)␈↓:␈α_Fixpoint␈α_Induction␈α_and␈α_Proofs␈α_of␈α_Program␈α_Properties",␈α_in␈α↔␈↓↓Machine
␈↓ ↓H␈↓↓Intelligence 5␈↓, pp. 59-78, Edinburgh University Press, Edinburgh.

␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Artificial Intelligence Laboratory
␈↓ ↓H␈↓Computer Science Department
␈↓ ↓H␈↓Stanford University
␈↓ ↓H␈↓Stanford, California 94305

␈↓ ↓H␈↓ARPANET: MCCARTHY@SU-AI

␈↓ ↓H␈↓␈↓εThis draft of FIRST.NEW[W77,JMC] PUBbed at 15:46 on April 10, 1977.␈↓